diff options
| author | Josh Chen | 2018-06-05 18:42:54 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-06-05 18:42:54 +0200 |
| commit | d09095bec2c136f600edd0039a1cc1eae441d823 (patch) | |
| tree | 693778613207b0cd5a79313b9c3ca104d9e08eab /HoTT_Theorems.thy | |
| parent | 80412abb0fdec553d80a56af16d1cfd8da52e7ed (diff) | |
Code formatting
Diffstat (limited to 'HoTT_Theorems.thy')
| -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 |