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

feat: also return true if term contain delayed assignments

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-16 19:53:11 -08:00
parent f6622b3120
commit 41a093f2df
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Lean/MetavarContext.lean
View file

@ -396,7 +396,7 @@ def hasAssignedLevelMVar (mctx : MetavarContext) : Level → Bool
| Level.zero _ => false
| Level.param _ _ => false
/-- Return `true` iff expression contains assigned (level/expr) metavariables -/
/-- Return `true` iff expression contains assigned (level/expr) metavariables or delayed assigned mvars -/
def hasAssignedMVar (mctx : MetavarContext) : Expr → Bool
| Expr.const _ lvls _ => lvls.any (hasAssignedLevelMVar mctx)
| Expr.sort lvl _ => hasAssignedLevelMVar mctx lvl
@ -409,7 +409,7 @@ def hasAssignedMVar (mctx : MetavarContext) : Expr → Bool
| Expr.lit _ _ => false
| Expr.mdata _ e _ => e.hasMVar && hasAssignedMVar e
| Expr.proj _ _ e _ => e.hasMVar && hasAssignedMVar e
| Expr.mvar mvarId _ => mctx.isExprAssigned mvarId
| Expr.mvar mvarId _ => mctx.isExprAssigned mvarId || mctx.isDelayedAssigned mvarId
| Expr.localE _ _ _ _ => unreachable!
/-- Return true iff the given level contains a metavariable that can be assigned. -/