Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-08-12

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

All times shown according to UTC.

Time Nick Message
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/
07:43 ski joined #isabelle
07:47 g0d355__ joined #isabelle
11:45 chuchucorny does Isabelle somewhere have a Monad class (comparable to haskell?)
13:23 JCaesar chuchucorny: No idea whether https://www.isa-afp.org/browser_info/current/AFP/ROBDD/Monad_Syntax.html has anything to do with what you're looking for… (~~/src/HOL/Library/Monad_Syntax)
13:24 JCaesar hm, probably not…
13:41 chuchucorny nope, thats just syntax
13:43 chuchucorny how can I debug an "Unresolved adhoc overloading of constant ..." error?
13:57 chuchucorny ahh, I have to call adhoc_overloading to get my bind implementation ready for monad syntax
15:40 larsrh chuchucorny: How would Isabelle have a monad class?
15:40 larsrh we don't have type constructor polymorphism
15:45 int-e which is why the monad syntax uses that horrible ad-hoc overloading instead :/
15:55 chindy is adhoc overloading something that is adviced to use?
16:04 int-e in small doses, maybe
16:06 larsrh it's ok-ish if you're happy to see indecipherable type error messages from time to time
16:06 larsrh and as I hear, syntax/locales/adhoc-overloading don't play well togheter
16:06 int-e (the group action in nominal isabelle may be a good example)
16:06 larsrh *together
16:12 int-e oh, right, I heard about that... something about internal syntax leaking through the pretty printer.
16:21 chindy any chance to add this lemma or something like this to the library? http://downthetypehole.de/paste/8ZvJ0tkY
16:22 chindy maybe it is present already, and i/sledgehammer could not find it
16:56 larsrh chuchucorny: that would be pruvisto's department
16:56 larsrh sorry, chindy: ---^
19:28 wagle joined #isabelle
19:55 chuchucorny Isabelle IO programming: https://github.com/diekmann/Isabelle-Hello-World
19:55 chuchucorny Who may I nerdsnipe?
20:15 D33P-B00K joined #isabelle
20:18 D33P-B00K left #isabelle
21:58 int-e . o O ( ITYM "whom" )
22:47 ilbot3 joined #isabelle
22: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/

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