diff options
Diffstat (limited to '')
-rw-r--r-- | HoTT_Theorems.thy | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index 1ac4484..52e1b32 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -141,6 +141,7 @@ consts Ui::Term definition Id where "Id \<equiv> \<^bold>\<lambda>A:Ui. \<^bold>\<lambda>x:A. x" (* Have to think about universes... *) +(* section \<open>Nats\<close> text "Here's a dumb proof that 2 is a natural number." @@ -156,5 +157,6 @@ text "We can of course iterate the above for as many applications of \<open>succ The next thing to do is to implement induction to automate such proofs. When we get more stuff working, I'd like to aim for formalizing the encode-decode method to be able to prove the only naturals are 0 and those obtained from it by \<open>succ\<close>." +*) end
\ No newline at end of file |