Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-07-02

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

All times shown according to UTC.

Time Nick Message
10:37 isabelle-bot joined #isabelle
10:41 larsrh now with timeout and truncation
10:43 int-e off with their heads!
10:43 int-e !value 20 * 20 :: nat
10:43 isabelle-bot int-e: Failed, probably timeout?
10:43 int-e (but I expect it chops off tails)
10:43 int-e !value 20 * 2 :: nat
10:44 isabelle-bot int-e: Failed, probably timeout?
10:44 int-e !value 2 * 2 :: nat
10:44 isabelle-bot int-e: Failed, probably timeout?
10:44 int-e well at least the timeout works!
10:46 larsrh heh
10:46 larsrh I didn't say the timeout was particularly large :p
10:47 isabelle-bot joined #isabelle
10:47 larsrh in all seriousness though, this wasn't as intended
10:47 larsrh !value 20 * 2 :: nat
10:47 isabelle-bot larsrh: Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (
10:47 int-e I assumed as much.
10:47 pruvisto I should finally fix printing of nat
10:47 pruvisto before the next release
10:47 int-e But it was funny. :)
10:47 larsrh int-e: it looks like Isabelle ignored my humble request to interrupt the thread
10:48 * larsrh gets out the pitchfork
10:48 int-e . o O ( !import Code_Target_Nat )
10:50 larsrh oh well, that's for another hacking session :-)
10:51 larsrh for now I blame PircBotX
14:32 ilbot3 joined #isabelle
14:32 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/
14:34 ilbot3 joined #isabelle
14:34 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/
16:48 mal`` joined #isabelle
19:31 qwertyyyy hi , why is "(⋀y .y = B ⟹ A) ⟹ A" true but "⋀y. (y = B ⟹ A) ⟹ A" not ?
21:06 pruvisto qwertyyyy: well, the second one means "∀y. ((y = B → A) → A)"
21:07 pruvisto and that is, in general, false, if one chooses some y ≠ B
21:08 pruvisto the first one means "(∀y. (y = b → A)) → A", which is true, since one can simply instantiate y = B.
21:08 keep_learning joined #isabelle
22:04 chindy What if in this case http://downthetypehole.de/paste/Hg7Q66YW (shown by int-e) A is not a locale but a typeclass how would that work ?

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