Documentation

Lean.Util.ReplaceLevel

partial def Lean.Level.replace (f? : LevelOption Level) (u : Level) :
@[reducible, inline]
Equations
    Instances For
      Instances For
        @[reducible, inline]
        Equations
          Instances For
            unsafe def Lean.Expr.ReplaceLevelImpl.cache (i : USize) (key result : Expr) :
            Equations
              Instances For
                Equations
                  Instances For
                    Equations
                      Instances For
                        Equations
                          Instances For
                            Equations
                              Instances For
                                @[implemented_by Lean.Expr.ReplaceLevelImpl.replaceUnsafe]
                                partial def Lean.Expr.replaceLevel (f? : LevelOption Level) :