Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-03-17

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

All times shown according to UTC.

Time Nick Message
02:51 fracting joined #isabelle
04:07 fracting joined #isabelle
05:39 fracting joined #isabelle
07:28 fracting joined #isabelle
07:58 fracting joined #isabelle
09:19 fracting joined #isabelle
11:19 Damaki joined #isabelle
11:23 Damaki joined #isabelle
11:50 Damaki !last
14:05 fracting joined #isabelle
17:34 Damaki joined #isabelle
17:45 ThreeOfEight larsrh: I'm having a strange issue here
17:46 ThreeOfEight I'm using local_theory_to_proof and Local_Theory.notes in the after_qed to register some theorems derived from the proven theorem as simp lemmas
17:46 ThreeOfEight but for some reason, the theorems are not in the simpset, no matter whether I use "addsimps" on the context or specify "[simp]" in the Local_Theory.notes
17:48 larsrh ThreeOfEight: But the theorem is bound to the name you've specified?
17:48 larsrh Or does it just not exist at all?
17:49 larsrh Do you look at the simpset while you're still in the command, or after the command is finished?
17:56 ThreeOfEight larsrh: yes, it is bound to that name
17:57 ThreeOfEight and I looked at it after the command is finished
17:59 larsrh ThreeOfEight: post it to the mailing list, maybe?
18:00 larsrh I just asked Makarius and he'd like to see the source
18:05 ThreeOfEight oh dear
18:06 ThreeOfEight http://downthetypehole.de/paste/P9r2NAL9
18:06 ThreeOfEight I also tried an "|> (fn ctxt => ctxt addsimps wf_thms)" at the end
18:07 ThreeOfEight that didn't do anything either
18:07 ThreeOfEight the relevant code is around line 320
23:07 larsrh ThreeOfEight: hmm, I don't see any obvious problems
23:07 larsrh For debugging I'd declare my own attribute which prints some debug output
23:07 larsrh Then you can see how it's being processed
23:10 larsrh It looks exactly like what BNF is doing

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