Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-01-22

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

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 meta-logical 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

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary