max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: isWellFormed

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-16 10:14:47 -07:00
parent d81f1c585b
commit d00dc1988a
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/MetavarContext.lean
View file

@ -996,10 +996,10 @@ mkBinding false xs e true
partial def isWellFormed (mctx : MetavarContext) (lctx : LocalContext) : Expr → Bool
| Expr.mdata _ e _ => isWellFormed e
| Expr.proj _ _ e _ => isWellFormed e
| e@(Expr.app f a _) => (e.hasExprMVar || e.hasFVar) && isWellFormed f && isWellFormed a
| e@(Expr.lam _ d b _) => (e.hasExprMVar || e.hasFVar) && isWellFormed d && isWellFormed b
| e@(Expr.forallE _ d b _) => (e.hasExprMVar || e.hasFVar) && isWellFormed d && isWellFormed b
| e@(Expr.letE _ t v b _) => (e.hasExprMVar || e.hasFVar) && isWellFormed t && isWellFormed v && isWellFormed b
| e@(Expr.app f a _) => (!e.hasExprMVar && !e.hasFVar) || (isWellFormed f && isWellFormed a)
| e@(Expr.lam _ d b _) => (!e.hasExprMVar && !e.hasFVar) || (isWellFormed d && isWellFormed b)
| e@(Expr.forallE _ d b _) => (!e.hasExprMVar && !e.hasFVar) || (isWellFormed d && isWellFormed b)
| e@(Expr.letE _ t v b _) => (!e.hasExprMVar && !e.hasFVar) || (isWellFormed t && isWellFormed v && isWellFormed b)
| Expr.const _ _ _ => true
| Expr.bvar _ _ => true
| Expr.sort _ _ => true