# IRC log for #isabelle, 2017-02-27

All times shown according to UTC.

Time Nick Message
00:03 chindy yea... as listing or ssomething, im kinda trying to use it in a latex beamer
02:47 ilbot3 joined #isabelle
02:47 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:23 larsrh chindy: pygments supports Isabelle
07:24 larsrh (it's now in upstream pygments)
07:24 larsrh and you can use ftp://ftp.dante.de/tex-archive/macros/latex/contrib/minted/minted.pdf to highlight via pygmentize in latex
07:36 ammbauer http://stackoverflow.com/a/42470178/7334861
07:37 ammbauer pruvisto: are there finitely many distinct lists over a finite set?
07:37 ammbauer the numbers 0 to 9 are finite and the lists over them are infinite, right?
07:40 larsrh distinct lists ... i.e. lists that have no duplicate elements
07:42 ammbauer larsrh: ahhh, okay.
07:49 ammbauer so lets count them [], [0], [1], [2], [3], [4], [5], [6], [7], [8], [9], [0,1], [0,2], [0,3],… … this may take a while. I'll be back in a sec :D
08:36 ammbauer …, [9,8,7,6,5,4,3,2,1,0] yep, seems to be finite
08:49 larsrh *trollface*
10:16 silver joined #isabelle
11:08 pruvisto ammbauer: pretty sure, seeing as I proved it in Isabelle before ;)
12:09 dmiles joined #isabelle
12:42 stoopkid joined #isabelle
17:07 silver_ joined #isabelle