Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-11-22

| 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/
02:52 ammbauer joined #isabelle
12:14 silver joined #isabelle
16:36 int-e is there a trick to get natural numbers displayed as numbers in Isabelle's output (jedit, output panel...) when evaluating expressions?
16:39 int-e Okay, this I can work with: converting to int helps.
16:45 larsrh int-e: I'm unaware of anything better than that
16:52 ammbauer importing "~~/src/HOL/Library/Code_Target_Nat"?
16:52 ammbauer https://stackoverflow.com/questions/22687646/simplify-pretty-printing-of-naturals
16:52 larsrh cool, TIL
17:03 int-e ammbauer: thanks, I didn't expect that ... uhm ... side effect.
17:52 ThreeOfEight int-e: I actually hacked something together for that a while ago
17:53 ThreeOfEight I was planning to put it into the distribution at some point
17:55 ThreeOfEight int-e: http://downthetypehole.de/paste/geC6Ll0U
17:55 ThreeOfEight This works.
17:55 ThreeOfEight Of course, the computations are a bit slow because this uses unary numbers internally
17:55 ThreeOfEight but it's enough for small examples
17:56 silver joined #isabelle
17:57 ThreeOfEight this also changes the output for quickcheck

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