Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-07-25

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
01:51 ilbot3 joined #isabelle
01:51 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
08:48 relrod joined #isabelle
08:48 relrod joined #isabelle
10:22 larsrh the year is 2020. the archive of formal proofs has been renamed to archive of formal pruvisto
10:50 stoopkid_ joined #isabelle
13:36 larsrh Ondrej and me just implemented a cute lil trick
13:36 larsrh fun bla where "bla (x =: (y # (x' =: (y' # ys)))) = x @ x'"
13:37 larsrh `=:` aka `as` in SML and `@` in Haskell
13:42 int-e how does that work?
13:44 larsrh the idea is that "f (x =: pat) = rhs" is translated to "f pat = (let x = pat in rhs)"
13:44 int-e so you adapt the function package?
13:45 larsrh no, it's a check phase
13:45 larsrh so we adapt the type cheker
13:45 larsrh *checker
13:45 larsrh well, we add another stage after type checking
17:06 aindilis joined #isabelle
17:43 pruvisto for anyone who things this sounds like a horrible hack: it is, but Isabelle has a few more hacks like this switched on by default anyway :P
21:59 mbrcknl_ joined #isabelle
22:59 stoopkid_ joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary