From d00dc1988a7105f5d0572f28c0f7ecb032b29663 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 16 Sep 2020 10:14:47 -0700 Subject: [PATCH] fix: `isWellFormed` --- src/Lean/MetavarContext.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index c40830b05f..638fc10a1d 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -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