Skip to content

Commit 19c5696

Browse files
authored
chore: add an assertion about mkValueTypeClosure
This is a guard against #10705
1 parent d5ca0c7 commit 19c5696

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/Lean/Meta/Closure.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -414,6 +414,7 @@ def mkValueTypeClosure (type : Expr) (value : Expr) (zetaDelta : Bool) : MetaM M
414414
let newLetDecls := s.newLetDecls.reverse
415415
let type := mkForall newLocalDecls (mkForall newLetDecls type)
416416
let value := mkLambda newLocalDecls (mkLambda newLetDecls value)
417+
assert! !value.hasFVar -- In case https://github.com/leanprover/lean4/issues/10705 resurfaces in a new way
417418
pure {
418419
type := type,
419420
value := value,

0 commit comments

Comments
 (0)