Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-02-28

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

All times shown according to UTC.

Time Nick Message
02:48 ilbot3 joined #isabelle
02: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:23 stoopkid joined #isabelle
04:35 tokenrove joined #isabelle
05:00 gk-1wm-su joined #isabelle
05:00 gk-1wm-su left #isabelle
11:49 silver joined #isabelle
14:31 dmiles joined #isabelle
15:03 JCaesar Hm, is there a typeclass for non-finite types?
15:34 stoopkid joined #isabelle
15:55 pruvisto JCaesar: I don't think so
16:22 JCaesar guess I'll go and have fun making one…
17:19 pruvisto JCaesar: what do you need that for?
17:25 trc joined #isabelle
17:26 trc Hi. I am wondering what UCARD is? In proving this lemma test: "length([1]) = 1" the output states: this subproof: UCARD([1]) = 1
17:26 trc why?
17:26 pruvisto trc: … I think there is some information missing here
17:27 pruvisto there is nothing called "UCARD" anywhere in the Isabelle repository or the AFP
17:27 pruvisto and the lemma "length [1] = 1" should be provable with "simp"
17:28 pruvisto so could you give a bit more context about what you are doing?
17:28 trc That is why I think it is weird pruvisto
17:28 pruvisto Are you using Isabelle/HOL?
17:28 pruvisto What theories do you have imported?
17:28 trc Yes, i'll create an entire pastebin
17:29 trc ah screaming baby.. sec
17:30 trc hmm okay, it is something I have imported.. sorry
17:31 pruvisto no worries
17:31 pruvisto still sounds odd though
17:33 trc Found it.. https://github.com/isabelle-utp/utp-main/blob/1d6aea4a00c9bd84fd0073fdb7be1693525b400c/utp/utp_expr.thy
17:33 trc I think
17:37 pruvisto okay I have no idea what that is
17:38 trc thanks though :)
22:08 silver joined #isabelle
22:25 stoopkid joined #isabelle
23:50 JCaesar pruvisto: propositional formulas, and I need something that allows producing "fresh" atoms.
23:50 JCaesar but I'm not so sure if I shouldn't just pack that into a locale…
23:50 JCaesar I'll probably discuss that with Tobias…

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