Documentation

Lean.Util.ReplaceLevel

partial def Lean.Level.replace (f? : LevelOption Level) (u : Level) :
Instances For
    unsafe def Lean.Expr.ReplaceLevelImpl.cache (i : USize) (key result : Expr) :
    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[implemented_by Lean.Expr.ReplaceLevelImpl.replaceUnsafe]
          partial def Lean.Expr.replaceLevel (f? : LevelOption Level) :