Time 
Nick 
Message 
01:09 
lispy 
ThreeOfEight: nice 
03:46 

dmiles_afk joined #isabelle 
03:56 

kini joined #isabelle 
04:39 
spacekitteh 
does isabelle/hol have function extensionality? 
06:47 
larsrh 
spacekitteh: yes, see 'thm ext' 
06:56 
ThreeOfEight 
spacekitteh: fyi, you can actually look at all of HOL's axioms where they are defined: http://isabelle.in.tum.de/repos/isabelle/file/5fb86150a579/src/HOL/HOL.thy 
06:57 
ThreeOfEight 
(e.g. ext is in line 169) 
06:59 
ThreeOfEight 
although I should probably say that Isabelle's meta logic already contains extensionality 
07:16 
ThreeOfEight 
Yes, ext actually follows from refl and eq_reflection (and the metalogical inference rule Thm.abstract_rule) 
07:16 
ThreeOfEight 
http://downthetypehole.de/paste/BfzHdtH8 
07:16 
ThreeOfEight 
(Don't try this at home.) 
08:00 

spacekitteh joined #isabelle 
08:03 
spacekitteh 
jnm, 
08:55 
spacekitteh 
thanks larsrh + ThreeOfEight 
08:56 
spacekitteh 
the logic i'm most familiar with is hott so it's a bit of a nuisance going back to classical simply typed logics :( 
15:47 

irctc396 joined #isabelle 
17:06 

ski joined #isabelle 
18:58 

Guest98671 joined #isabelle 
19:27 

ammbauer joined #isabelle 