diff options
| author | stuebinm | 2022-06-29 01:28:53 +0200 |
|---|---|---|
| committer | stuebinm | 2022-06-29 01:28:53 +0200 |
| commit | 4fd7d22b0efb69bc13c43dae4e4c1bd6d392f37d (patch) | |
| tree | 2819976f3fe60d2e9796ec37d2b0736df55daa59 /hott/Nat.thy | |
| parent | cb4139dc35527bd8c8f9b70753c3d1f552c5f19d (diff) | |
this just replaces all instance of `this` with instances of `infer`.
Unfortunately, it looks likes something else also broke, and I have
no idea what it is (but the proof for equiv_if_equal fails).
Sadly this means we can't get to univalence for now …
(but rn I'm too tired to try anything else with it)
Diffstat (limited to 'hott/Nat.thy')
| -rw-r--r-- | hott/Nat.thy | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/hott/Nat.thy b/hott/Nat.thy index 33a5d0a..0a38f99 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -115,7 +115,7 @@ Lemma (def) add_comm: proof compute have "suc (m + n) = suc (n + m)" by (eq ih) refl also have ".. = suc n + m" by (rewr eq: suc_add) refl - finally show "?" by this + finally show "?" by infer qed done @@ -152,7 +152,7 @@ Lemma (def) zero_mul: proof compute have "0 + 0 * n = 0 + 0 " by (eq ih) refl also have ".. = 0" by compute refl - finally show "?" by this + finally show "?" by infer qed done @@ -165,7 +165,7 @@ Lemma (def) suc_mul: proof (compute, rewr eq: \<open>ih:_\<close>) have "suc m + (m * n + n) = suc (m + ?)" by (rule suc_add) also have ".. = suc (m + m * n + n)" by (rewr eq: add_assoc) refl - finally show "?" by this + finally show "?" by infer 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 (rewr eq: add_comm) refl also have ".. = l * m + (l + l * n)" by (rewr eq: add_assoc) refl - finally show "?" by this + finally show "?" by infer qed done @@ -193,7 +193,7 @@ Lemma (def) mul_assoc: proof compute have "l * (m + m * n) = l * m + l * (m * n)" by (rule mul_dist_add) also have ".. = l * m + l * m * n" by (rewr eq: \<open>ih:_\<close>) refl - finally show "?" by this + finally show "?" by infer 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 (rewr eq: \<open>ih:_\<close>, rewr eq: add_comm) refl - finally show "?" by this + finally show "?" by infer qed done |