diff options
author | Josh Chen | 2021-01-18 23:49:13 +0000 |
---|---|---|
committer | Josh Chen | 2021-01-18 23:49:13 +0000 |
commit | f46df86db9308dde29e0e5f97f54546ea1dc34bf (patch) | |
tree | b9523698c4ec81f3bba8f6b549d386505e345746 /hott/Nat.thy | |
parent | 3922e24270518be67192ad6928bb839132c74c07 (diff) |
Swapped notation for metas (now ?) and holes (now {}), other notation and name changes.
Diffstat (limited to 'hott/Nat.thy')
-rw-r--r-- | hott/Nat.thy | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/hott/Nat.thy b/hott/Nat.thy index f45387c..1aa7932 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -115,7 +115,7 @@ Lemma (def) add_comm: proof reduce have "suc (m + n) = suc (n + m)" by (eq ih) refl also have ".. = suc n + m" by (transport eq: suc_add) refl - finally show "{}" by this + finally show "?" by this qed done @@ -152,7 +152,7 @@ Lemma (def) zero_mul: proof reduce have "0 + 0 * n = 0 + 0 " by (eq ih) refl also have ".. = 0" by reduce refl - finally show "{}" by this + finally show "?" by this qed done @@ -163,9 +163,9 @@ Lemma (def) suc_mul: \<^item> by reduce refl \<^item> vars n ih proof (reduce, transport eq: \<open>ih:_\<close>) - have "suc m + (m * n + n) = suc (m + {})" by (rule suc_add) + have "suc m + (m * n + n) = suc (m + ?)" by (rule suc_add) also have ".. = suc (m + m * n + n)" by (transport eq: add_assoc) refl - finally show "{}" by this + finally show "?" by this qed done @@ -180,7 +180,7 @@ Lemma (def) mul_dist_add: also have ".. = l + l * m + l * n" by (rule add_assoc) also have ".. = l * m + l + l * n" by (transport eq: add_comm) refl also have ".. = l * m + (l + l * n)" by (transport eq: add_assoc) refl - finally show "{}" by this + finally show "?" by this qed done @@ -193,7 +193,7 @@ Lemma (def) mul_assoc: proof reduce have "l * (m + m * n) = l * m + l * (m * n)" by (rule mul_dist_add) also have ".. = l * m + l * m * n" by (transport eq: \<open>ih:_\<close>) refl - finally show "{}" by this + finally show "?" by this qed done @@ -207,7 +207,7 @@ Lemma (def) mul_comm: have "suc n * m = n * m + m" by (rule suc_mul) also have ".. = m + m * n" by (transport eq: \<open>ih:_\<close>, transport eq: add_comm) refl - finally show "{}" by this + finally show "?" by this qed done |