Documentation

Lean.Util.FoldConsts

@[inline, reducible]
Equations
Instances For
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        unsafe def Lean.Expr.FoldConstsImpl.fold {α : Type} (f : Lake.Nameαα) (size : USize) (e : Lean.Expr) (acc : α) :
        Equations
        Instances For
          unsafe def Lean.Expr.FoldConstsImpl.fold.visit {α : Type} (f : Lake.Nameαα) (size : USize) (e : Lean.Expr) (acc : α) :
          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.FoldConstsImpl.foldUnsafe]
              opaque Lean.Expr.foldConsts {α : Type} (e : Lean.Expr) (init : α) (f : Lake.Nameαα) :
              α

              Apply f to every constant occurring in e once.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For