# IRC log for #isabelle, 2017-04-11

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/
02:33 stoopkid joined #isabelle
05:51 pruvisto okay monoid_mult /isn't/ enough because you can't do "2 * …"
05:51 pruvisto you'd have to rewrite your function without the 2* and then it would work
05:51 pruvisto JCaesar: so, I trust you found and proved the solution?
05:53 pruvisto int-e: my guess is that it has something to do with it being defined in a type class
07:01 JCaesar pruvisto: Did. k*2^(2^n).
07:02 pruvisto yup
07:02 pruvisto primrec works fine, too
07:02 pruvisto by (induction n arbitrary: k) (simp_all add: semiring_normalization_rules(36))
07:09 JCaesar interestingly, my sledgehammer used number 26 instead of 36…
07:15 pruvisto That's Numberwang!
07:21 larsrh ouch, there seems to be even more fallout from the LDAP problem
07:54 dave24 joined #isabelle
09:11 dave24 is there a logarithm function?
09:18 dave24 nvm found it
09:18 JCaesar what's it called?
09:23 dave24 its in http://isabelle.in.tum.de/library/HOL/HOL/Transcendental.html
09:23 dave24 called just log
09:24 dave24 and theres one for natural numbers as well: http://isabelle.in.tum.de/library/HOL/HOL-Library/Log_Nat.html
09:27 JCaesar ah. :)
10:18 pruvisto there's also ln
10:19 pruvisto and then there's Discrete.log, which I think is essentially "natlog 2"
10:19 pruvisto not sure if bitlen still exists, that was also more or less "natlog 2", iirc
10:35 silver joined #isabelle
14:01 stoopkid joined #isabelle
15:00 larsrh I just created a datatype plugin that generates the following theorem:
15:00 larsrh Typerep.typerep.Typerep_def: Typerep.Typerep.typerep.Typerep ≡ typerep.Typerep
15:05 pruvisto Lovely.
16:06 JCaesar wtf? meson is capable of not solving goals?
16:06 JCaesar I do an apply meson, I have one subgoal before and one after.
16:06 JCaesar and sledgehammer claims that by meson would solve the goal.
16:07 JCaesar metis does solve it. O_O
17:43 JCaesar Hm, does anybody know what kind of goat I have to sacrifice to get proper list comprehensions in latex output?
20:05 pruvisto JCaesar: what do you mean by "proper"?
20:05 JCaesar actually… existent would be enough…
20:06 pruvisto hm
20:06 JCaesar (i've already sprayed a version of the id function that gets printed to nothing to avoid eta-contractions all over the place, so that should not be a problem.)
20:07 pruvisto "filter" usually pretty-prints as a list comprehension for me
20:07 pruvisto don't know about the rest
20:07 pruvisto I don't use the LaTeX output
20:34 JCaesar I proved some lemma on [foo a b. a <- A, b <- B]. it gets printed as concat (map (λ a. map (λ b. foo a b))).
20:35 JCaesar I wonder if I can just define some constant and then give that an appropriate printing…
22:59 stoopkid joined #isabelle
23:09 chindy what is \longrightarrow? and how is continuous F f defined using a said arrow ?
23:41 chindy should f22 follow quite simply ? http://downthetypehole.de/paste/BImdLQzm