Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-05-02

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

All times shown according to UTC.

Time Nick Message
01:48 ilbot3 joined #isabelle
01: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/
02:43 wagle joined #isabelle
06:53 ertes joined #isabelle
08:03 dave24 joined #isabelle
09:24 ertes joined #isabelle
10:21 notdan left #isabelle
11:06 ertes joined #isabelle
11:23 trc joined #isabelle
11:26 trc I have typedef 'a lpf = "UNIV :: 'a option set" and I am trying to instantiate it for modulos. instantiation lpf :: ("{zero,divide,times}") modulo . However, I get the error: Cannot derive subsort relation {times,zero,divide} < modulo.
11:26 trc Can anyone explain to me why?
11:46 pruvisto Cannot reproduce under Isabelle2016-1
11:46 pruvisto my guess would be that you have other "instantiation"s for lpf before that one
11:47 pruvisto and then that instantiation violates coregularity
11:52 trc Ah
11:52 trc solved it
11:52 trc I needed {zero,divide,modulo}
11:52 trc as constraints
11:53 pruvisto sounds like the coregularity restriction
11:53 pruvisto or, as I call it, "type class instance sudoku"
12:28 trc hehe nice work for it
13:11 ertes joined #isabelle
14:47 hazyPurple joined #isabelle
15:06 kyagrd joined #isabelle
15:08 tautologico joined #isabelle
15:49 hazyPurple joined #isabelle
16:26 ertes joined #isabelle
17:52 logicmoo joined #isabelle
20:59 ertesx joined #isabelle

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