# IRC log for #isabelle, 2016-03-15

All times shown according to UTC.

Time Nick Message
02:10 fracting joined #isabelle
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/
03:08 fracting joined #isabelle
03:25 JCaesar Oha. apply(clarsimp split: a b) succeeds but apply(clarsimp split: b a) produces an unsolvable subgoal.
03:25 JCaesar (Okay, I'm doing evil magic with if_splits, Option.bind_splits and _ ← (if foo then Some () else None). Still, I didn't expect that.)
03:28 fracting joined #isabelle
04:57 fracting joined #isabelle
05:17 JCaesar btw, is there a use for \$ being less binding than the ; of a let or do?
08:27 fracting joined #isabelle
08:27 dmiles joined #isabelle
08:42 fracting joined #isabelle
09:10 ThreeOfEight JCaesar: what do you mean by \$?
09:11 JCaesar op \$
09:11 ThreeOfEight What operator is that?
09:11 ThreeOfEight I know that as the coefficient of a formal power series
09:11 ThreeOfEight but I doubt you're using formal power series
09:12 larsrh ThreeOfEight: I suppose JCaesar is suggesting the introduction of a Haskell-like \$ operator
09:26 ThreeOfEight oh
09:26 ThreeOfEight well the way he phrased it, it sounded like this \$ already existed in Isabelle
09:27 ThreeOfEight in any case, I don't see how it could possibly extend past the ";" of a let without yielding invalid syntax
10:04 JCaesar Eeeh… It's called fun_app, and it exists…
10:04 JCaesar (The question is where though.)
10:09 larsrh grepping over src/HOL reveals src/HOL/Library/Old_SMT.thy:definition fun_app where "fun_app f = f"
10:09 larsrh followed by hide_const
10:24 fracting joined #isabelle
10:24 larsrh JCaesar: If you want you can just declare an input abbreviation for id
10:29 fracting joined #isabelle
10:32 fracting joined #isabelle
10:32 larsrh JCaesar: abbreviation (input) funapp :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b" (infixl "\$" 0) where "funapp f x ≡ f x"
10:36 JCaesar ah, the nicta people defined it…
10:36 JCaesar ic…
10:36 JCaesar Then the question is… why was I able to use it in the BDD stuff. *goes to find out*
10:40 ThreeOfEight JCaesar: just ctrl-click on it?
10:40 ThreeOfEight oh, you're trying to see the include-chain?
10:45 larsrh use command thy_deps
10:48 fracting joined #isabelle
10:52 fracting joined #isabelle
10:55 fracting1 joined #isabelle
11:19 fracting1 joined #isabelle
13:29 ilbot3 joined #isabelle
13:29 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/
15:04 fracting1 joined #isabelle
16:00 fracting1 joined #isabelle
17:34 fracting1 joined #isabelle