summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-12-12 17:47:58 +0100
committerSon Ho2023-12-12 17:47:58 +0100
commit698f631e7addb92eb270a75607f1f6ffd8b2414f (patch)
tree2502245d112fb66f33889a6ab4a15a4afd6607f6
parentdba35a41e66019e586502f563ce7c629356fb2d7 (diff)
Fix minor issues with the divergence encoding
-rw-r--r--backends/lean/Base/Diverge/Elab.lean19
1 files changed, 5 insertions, 14 deletions
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index 08d21e42..e9544f38 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -899,8 +899,11 @@ partial def proveAppIsValidApplyThms (k_var kk_var : Expr) (e : Expr)
lambdaOne e_lam.consumeMData fun kk_var e => do
-- Continue
trace[Diverge.def.valid] "kk_var: {kk_var}\ne: {e}"
- -- We sometimes need to reduce the term
- let e ← whnf e
+ -- We sometimes need to reduce the term - TODO: this is really dangerous
+ let e ← do
+ let updt_config config :=
+ { config with transparency := .reducible, zetaNonDep := false }
+ withConfig updt_config (whnf e)
trace[Diverge.def.valid] "e (after reduction): {e}"
let e_valid ← proveExprIsValid k_var kk_var e
trace[Diverge.def.valid] "e_valid (for e): {e_valid}"
@@ -1450,10 +1453,6 @@ namespace Tests
#check id.unfold
- -- set_option pp.explicit true
- -- set_option trace.Diverge.def true
- -- set_option trace.Diverge.def.genBody true
- set_option trace.Diverge.def.valid true
divergent def id1 {a : Type u} (t : Tree a) : Result (Tree a) :=
match t with
| .leaf x => .ret (.leaf x)
@@ -1464,12 +1463,6 @@ namespace Tests
#check id1.unfold
- /-set_option trace.Diverge.def false
-
- -- set_option pp.explicit true
- -- set_option trace.Diverge.def true
- -- set_option trace.Diverge.def.genBody true
- set_option trace.Diverge.def.valid true
divergent def id2 {a : Type u} (t : Tree a) : Result (Tree a) :=
match t with
| .leaf x => .ret (.leaf x)
@@ -1480,8 +1473,6 @@ namespace Tests
#check id2.unfold
- set_option trace.Diverge.def false -/
-
/-set_option trace.Diverge.def true
-- set_option trace.Diverge.def.genBody true
set_option trace.Diverge.def.valid true