HepLean Documentation

Lean.Util.ReplaceLevel

source
partial def Lean.Level.replace (f? : Lean.Level → Option Lean.Level) (u : Lean.Level) :
Lean.Level
source
@[reducible, inline]
abbrev Lean.Expr.ReplaceLevelImpl.cacheSize :
USize
Equations
Instances For
    source
    structure Lean.Expr.ReplaceLevelImpl.State :
    Type
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Expr.ReplaceLevelImpl.ReplaceM (α : Type) :
      Type
      Equations
      Instances For
        source
        unsafe def Lean.Expr.ReplaceLevelImpl.cache (i : USize) (key : Lean.Expr) (result : Lean.Expr) :
        Lean.Expr.ReplaceLevelImpl.ReplaceM Lean.Expr
        Instances For
          source
          unsafe def Lean.Expr.ReplaceLevelImpl.replaceUnsafeM (f? : Lean.Level → Option Lean.Level) (size : USize) (e : Lean.Expr) :
          Lean.Expr.ReplaceLevelImpl.ReplaceM Lean.Expr
          Instances For
            source
            unsafe def Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit (f? : Lean.Level → Option Lean.Level) (size : USize) (e : Lean.Expr) :
            Lean.Expr.ReplaceLevelImpl.ReplaceM Lean.Expr
            Instances For
              source
              unsafe def Lean.Expr.ReplaceLevelImpl.initCache :
              Lean.Expr.ReplaceLevelImpl.State
              Instances For
                source
                unsafe def Lean.Expr.ReplaceLevelImpl.replaceUnsafe (f? : Lean.Level → Option Lean.Level) (e : Lean.Expr) :
                Lean.Expr
                Instances For
                  source
                  @[implemented_by Lean.Expr.ReplaceLevelImpl.replaceUnsafe]
                  partial def Lean.Expr.replaceLevel (f? : Lean.Level → Option Lean.Level) :
                  Lean.Expr → Lean.Expr