Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-11-07

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

All times shown according to UTC.

Time Nick Message
02:47 ilbot3 joined #isabelle
02:47 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:30 dmiles joined #isabelle
13:32 silver joined #isabelle
15:46 mbrcknl joined #isabelle
17:33 JCaesar Hm, is there something similar to enum, just for infinite types?
17:52 JCaesar Or a way to easily show the existence a surjective function from nat to some my datatype?
18:31 larsrh JCaesar: you want to prove that something is countable?
18:32 larsrh try importing "~~/src/HOL/Library/Countable", there's a "countable" class in there
18:33 larsrh there's even a tactic in there for automatically proving countable-ness
18:45 ThreeOfEight larsrh: that countable_datatype tactic is pretty neat
18:45 ThreeOfEight But why isn't there a corresponding "untable_datatype" tactic?
19:00 larsrh ThreeOfEight: this joke never gets old, does it?
19:25 JCaesar that tictac is very nice, indeed.
19:28 JCaesar now, if from_nat could be evaluated (preferrably efficient), that would be amazing. "and here, I show you example 42785031"
19:32 ski joined #isabelle

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