add test file

leanprover · May 17, 2024 · d009ccd · d009ccd
1 parent 4dba92e
commit d009ccd
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 0 deletions.
diff --git a/tests/lean/syntheticOpaqueReadOnly.lean b/tests/lean/syntheticOpaqueReadOnly.lean
@@ -0,0 +1,12 @@
+import Lean
+
+open Lean Meta
+
+-- In a new MCtx depth, metavariables should not be assignable by `isDefEq`.
+
+run_meta do
+  let m ← mkFreshExprMVar (Expr.sort levelOne) MetavarKind.syntheticOpaque
+  withAssignableSyntheticOpaque do
+  withNewMCtxDepth do
+  let eq ← isDefEq m (.const ``Nat [])
+  Lean.logInfo m! "{eq}"
diff --git a/tests/lean/syntheticOpaqueReadOnly.lean.expected.out b/tests/lean/syntheticOpaqueReadOnly.lean.expected.out
@@ -0,0 +1 @@
+false