Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-12-10

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

All times shown according to UTC.

Time Nick Message
02:48 ilbot3 joined #isabelle
02:48 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/
10:06 silver joined #isabelle
12:49 fracting joined #isabelle
13:21 aindilis2 joined #isabelle
21:18 aindilis2 joined #isabelle
23:23 seafood joined #isabelle
23:24 seafood I’m wondering if someone could tell me more about why functions in HOL have to be total.
23:24 seafood If you could start out with a beginner answer and then build up to an expert one that would be great.
23:25 seafood My uninformed sense is that it has something to do with not complicating the semantics of functions with bottom (which is harder to reason about).
23:25 seafood But I feel I might be misguided

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