Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-02-13

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

All times shown according to UTC.

Time Nick Message
00:00 tangentstorm try ... by (simp only: add)
00:00 tangentstorm or add_def
00:00 tangentstorm (it autogenerates a name, but i don't remember the exact naming convention. sorry. :/)
00:01 tangentstorm by (simp only: add_def)   (* <- try that, crc_ *)
00:08 int-e is add defined by `fun` or `primrec`? if so, don't use add_def; use add.simps instead
00:13 crc_ thanks
10:15 ThreeOfEight "apply (subst add.simps)" for single-step rewriting
10:15 ThreeOfEight "apply (rule add.simps)" for resolution with add.simps, (i.e. "applying" the rule)
23:27 crc_ joined #isabelle

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