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 Haskelllike $ 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 ctrlclick on it? 
10:40 
ThreeOfEight 
oh, you're trying to see the includechain? 
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 