Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-01-25

| 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/
07:07 trc2 joined #isabelle
07:27 dmiles joined #isabelle
08:42 ammbauer left #isabelle
08:57 ammbauer joined #isabelle
11:31 silver joined #isabelle
14:05 JCaesar hm, btw, is there some way to say @{thm foo.simps} and have isabelle automatically align them on the =?
14:10 pruvisto um I guess you can do it by hand?
14:10 pruvisto take apart the conclusion of the theorem, pretty print the lhs and rhs, and pretty-print them
14:11 larsrh that's going to be difficult
14:11 larsrh afaik the Isabelle pretty-printer doesn't have vertical alignment
14:15 pruvisto true, and it's not a fixed-with font either
14:15 pruvisto *width
14:16 pruvisto so I guess aligning doesn't really work out well in general unless you have some editor support for it
14:46 JCaesar pruvisto: No, this is about the latex-generated code.
14:47 larsrh Define your own document antiquotatino?
14:47 larsrh *antiquotation
14:49 JCaesar I guess that's possible…
14:50 JCaesar I was kinda hoping I would get off with a [mode=foobar] or similar… but oh well…
14:50 JCaesar (Also, has nobody ever done this before?)
14:59 int-e does editing snippets by hand count...
16:15 pruvisto JCaesar: you could probably set up some special LaTeX output syntax for "="
16:16 pruvisto or add additional "pseudo-constants" into your HOL equation term that gets special LaTeX printing
16:16 pruvisto but I guess I'd just do it by hand
16:16 pruvisto Actually, my recommendation about Isabelle LaTeX output is "don't"
16:16 JCaesar Sorry, I'm writing a conference paper that way…
16:17 pruvisto I try to avoid Isabelle listings in my PDFs, and when I do have them, I typeset them entirely by hand
16:17 JCaesar And that might actually work… have a special printing rule for = :: bool => bool => bool that is only activated on a certain mode=…
18:08 chindy joined #isabelle

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