← Copula mathematical handbook

@[reducible, inline]

abbrev Lean.FindLevelMVar.Visitor : Type

Equations

• Lean.FindLevelMVar.Visitor = (Option Lean.LMVarId → Option Lean.LMVarId)

partial def Lean.FindLevelMVar.visit (p : LMVarId → Bool) (e : Expr) : Visitor

partial def Lean.FindLevelMVar.main (p : LMVarId → Bool) : Expr → Visitor

partial def Lean.FindLevelMVar.visitLevel (p : LMVarId → Bool) (l : Level) : Visitor

partial def Lean.FindLevelMVar.mainLevel (p : LMVarId → Bool) : Level → Visitor

@[inline]

def Lean.Expr.findLevelMVar? (e : Expr) (p : LMVarId → Bool) : Option LMVarId

Equations

• e.findLevelMVar? p = Lean.FindLevelMVar.main p e none