Documentation

Lean.Util.FindLevelMVar

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