Add test for #5667

leanprover · Oct 10, 2024 · 10d5081 · 10d5081
1 parent b814be6
commit 10d5081
Showing 1 changed file with 31 additions and 0 deletions.
diff --git a/tests/lean/run/issue5667.lean b/tests/lean/run/issue5667.lean
@@ -0,0 +1,31 @@
+inductive Expr where
+  | const (i : BitVec 32)
+  | op (op : Unit) (e1 : Expr)
+
+-- fails:
+
+def optimize : Expr → Expr
+  | .const i => .const i
+  | .op bop e1 =>
+    match bop, optimize e1 with
+    | _, .const _ => .op bop (.const 0)
+    | _, _ => .const 0
+termination_by structural e => e
+
+set_option trace.Elab.definition.structural.eqns true
+set_option trace.Elab.definition.wf.eqns true
+
+#check optimize.eq_2
+
+def optimize2 : Expr → Expr
+  | .const i => .const i
+  | .op bop e1 =>
+    match bop, optimize2 e1 with
+    | _, .const _ => .op bop (.const 0)
+    | _, _ => .const 0
+termination_by e => e
+
+set_option trace.Elab.definition.structural.eqns true
+set_option trace.Elab.definition.wf.eqns true
+
+#check optimize2.eq_2