Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-05-17

| 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/
03:36 fowlslegs joined #isabelle
04:52 keep_learning joined #isabelle
06:41 keep_learning Hi Everyone
06:42 keep_learning I am trying to prove https://github.com/mukeshtiwari/Isabelle/blob/master/Chap2.thy#L116 from http://www.concrete-semantics.org/concrete-semantics-brick.pdf page 19
06:42 keep_learning I am wondering if listsum is library function or I have to define it ?
06:43 keep_learning Also I am getting http://lpaste.net/355619
06:44 keep_learning When I am applying simp, listsum [] is not simplifying to 0
06:54 lispy joined #isabelle
06:55 pruvisto keep_learning: what Isabelle version?
06:56 pruvisto listsum was renamed to sum_list a while ago.
06:58 keep_learning pruvisto: I have the latest version 2016-1
06:59 keep_learning Thank you
07:24 wagle joined #isabelle
18:43 Guest67900 joined #isabelle
19:50 ski joined #isabelle
20:22 ertes joined #isabelle
21:04 ertes joined #isabelle

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