test: first pass

leanprover · Feb 23, 2024 · 98ebaa8 · 98ebaa8
1 parent ef75247
commit 98ebaa8
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/tests/lean/isDefEqDelayedMVarsBug.lean b/tests/lean/isDefEqDelayedMVarsBug.lean
@@ -0,0 +1,12 @@
+import Lean
+
+open Lean Meta Elab Tactic in
+elab "test " stx:term : tactic => withMainContext do
+  let e ← elabTerm stx none
+  discard <| withAssignableSyntheticOpaque <| isDefEq e (← getMainTarget)
+
+axiom F {α} : α → Prop
+
+theorem x : F (fun _ : Nat => 2) := by
+  test F (fun _ : Nat => ?e)
+  admit