← Mathematical handbook

def Lean.Meta.hasAssignableLevelMVar : Level → MetaM Bool

Equations

• Lean.Meta.hasAssignableLevelMVar lvl.succ = (pure lvl.hasMVar <&&> Lean.Meta.hasAssignableLevelMVar lvl)
• Lean.Meta.hasAssignableLevelMVar (lvl₁.max lvl₂) = (pure lvl₁.hasMVar <&&> Lean.Meta.hasAssignableLevelMVar lvl₁ <||> pure lvl₂.hasMVar <&&> Lean.Meta.hasAssignableLevelMVar lvl₂)
• Lean.Meta.hasAssignableLevelMVar (lvl₁.imax lvl₂) = (pure lvl₁.hasMVar <&&> Lean.Meta.hasAssignableLevelMVar lvl₁ <||> pure lvl₂.hasMVar <&&> Lean.Meta.hasAssignableLevelMVar lvl₂)
• Lean.Meta.hasAssignableLevelMVar (Lean.Level.mvar mvarId) = Lean.isLevelMVarAssignable mvarId
• Lean.Meta.hasAssignableLevelMVar Lean.Level.zero = pure false
• Lean.Meta.hasAssignableLevelMVar (Lean.Level.param a) = pure false

def Lean.Meta.hasAssignableMVar (e : Expr) : MetaM Bool

Return true iff expression contains a metavariable that can be assigned.

Equations

• Lean.Meta.hasAssignableMVar e = if (!e.hasMVar) = true then pure false else (Lean.Meta.hasAssignableMVar.go✝ e).run' ∅