summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
authorSon Ho2023-06-26 23:41:01 +0200
committerSon Ho2023-06-26 23:41:01 +0200
commit7f3604c21bb9f923aecb98917b5c7a33bafd1bcb (patch)
treeec49ec1718b592beda888c551bc81ace111d42ca /backends/lean
parentf4ee75da0959ff06ce4cfaab817de540fcd0433f (diff)
Make minor modifications
Diffstat (limited to 'backends/lean')
-rw-r--r--backends/lean/Base/Diverge.lean16
1 files changed, 0 insertions, 16 deletions
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index 907075d7..f3fa4815 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -522,20 +522,6 @@ namespace FixI
def is_valid (f : ((i:id) → a i → Result (b i)) → (i:id) → a i → Result (b i)) : Prop :=
∀ k i x, is_valid_p k (λ k => f k i x)
- @[simp] theorem kk_to_gen_kk_of_gen
- (k : (x: (i:id) × a i) → Result (b x.fst)) :
- kk_to_gen (kk_of_gen kk) = kk := by
- simp [kk_to_gen, kk_of_gen]
-
- @[simp] theorem k_to_gen_k_of_gen
- (k : ((x: (i:id) × a i) → Result (b x.fst)) → (x: (i:id) × a i) → Result (b x.fst)) :
- k_to_gen (k_of_gen kk) = kk := by
- simp [k_to_gen, k_of_gen]
- apply funext
- intro kk_1
- -- TODO: some simplifications don't work
- simp [kk_to_gen, kk_of_gen]
-
noncomputable def fix
(f : ((i:id) → a i → Result (b i)) → (i:id) → a i → Result (b i)) :
(i:id) → a i → Result (b i) :=
@@ -548,10 +534,8 @@ namespace FixI
have Hvalid' : Fix.is_valid (k_to_gen f) := by
intro k x
simp [is_valid, is_valid_p] at Hvalid
- --simp [Fix.is_valid_p]
let ⟨ i, x ⟩ := x
have Hvalid := Hvalid (k_of_gen k) i x
- -- TODO: some simplifications don't work
simp [k_to_gen, k_of_gen, kk_to_gen, kk_of_gen] at Hvalid
refine Hvalid
have Heq := Fix.is_valid_fix_fixed_eq Hvalid'