Documentation

Lean.Util.FindLevelMVar

source
@[reducible, inline]
abbrev Lean.FindLevelMVar.Visitor :
Type
Equations
    Instances For
      source
      partial def Lean.FindLevelMVar.visit (p : LMVarId → Bool) (e : Expr) :
      Visitor
      source
      partial def Lean.FindLevelMVar.main (p : LMVarId → Bool) :
      Expr → Visitor
      source
      partial def Lean.FindLevelMVar.visitLevel (p : LMVarId → Bool) (l : Level) :
      Visitor
      source
      partial def Lean.FindLevelMVar.mainLevel (p : LMVarId → Bool) :
      Level → Visitor
      source
      @[inline]
      def Lean.Expr.findLevelMVar? (e : Expr) (p : LMVarId → Bool) :
      Option LMVarId
      Equations
        Instances For