Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-08-09

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

All times shown according to UTC.

Time Nick Message
01:39 seafood joined #isabelle
01:39 seafood I was wondering if someone could help me out with Section 3.3 of https://isabelle.in.tum.de/doc/codegen.pdf
01:40 seafood We are asked to specify a conversion between the concrete type and an abstract type, and then the next line is "Dlist :: 'a list ? 'a dlist". However, this isn't valid Isabelle
01:41 seafood I can't just type that into jEdit and have it work.
01:41 seafood So what do I actually need to type here?
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/
04:21 seafood joined #isabelle
09:13 chindy seafood: not sure about the context but you probably need brackets like: (Dlist :: 'a list => 'a dlist)
10:15 numee joined #isabelle
10:43 silver joined #isabelle
12:09 chindy why doesn't this lemma work without nats?
12:09 chindy lcm_pos_nat
13:04 JCaesar chindy: what do you want it to work with?
13:05 JCaesar You need something to make the < make sense, and something to make the 0 make senseā€¦
13:18 JCaesar Hm, maybe {linorder, ring, gcd}?
14:19 pruvisto yeah that isn't going to work
14:20 pruvisto for a nat it holds trivially
14:20 pruvisto for int it holds because it was defined that way
14:20 pruvisto its completely arbitrary
14:21 pruvisto and I cant think of any other structure where it even makes any sense
23:30 keep_learning joined #isabelle

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