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

feat: add hasAssignableLevelMVar

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-30 18:23:30 -07:00
parent a9f3aa086d
commit e32402513d
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/Init/Lean/AbstractMetavarContext.lean
View file

@ -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₂)