Documentation

Lean.Meta.HasAssignableMVar

source
def Lean.Meta.hasAssignableLevelMVar :
Level → MetaM Bool
Instances For
    source
    def Lean.Meta.hasAssignableMVar (e : Expr) :
    MetaM Bool

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

    Instances For