From e32402513d66fe470317e52af10d375a616d0bd8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Oct 2019 18:23:30 -0700 Subject: [PATCH] feat: add `hasAssignableLevelMVar` --- library/Init/Lean/AbstractMetavarContext.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/library/Init/Lean/AbstractMetavarContext.lean b/library/Init/Lean/AbstractMetavarContext.lean index 2fd8351eff..f295734c0b 100644 --- a/library/Init/Lean/AbstractMetavarContext.lean +++ b/library/Init/Lean/AbstractMetavarContext.lean @@ -131,6 +131,16 @@ variables {σ : Type} [AbstractMetavarContext σ] @[inline] def isExprAssigned (mctx : σ) (mvarId : Name) : Bool := (getExprAssignment mctx mvarId).isSome +/-- Return true iff the given level contains a non-readonly metavariable. -/ +def hasAssignableLevelMVar (mctx : σ) : Level → Bool +| Level.succ lvl => lvl.hasMVar && hasAssignableLevelMVar lvl +| Level.max lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignableLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignableLevelMVar lvl₂) +| Level.imax lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignableLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignableLevelMVar lvl₂) +| Level.mvar mvarId => !isReadOnlyLevelMVar mctx mvarId +| Level.zero => false +| Level.param _ => false + +/-- Return true iff the given level contains an assigned metavariable. -/ def hasAssignedLevelMVar (mctx : σ) : Level → Bool | Level.succ lvl => lvl.hasMVar && hasAssignedLevelMVar lvl | Level.max lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignedLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignedLevelMVar lvl₂)