Documentation

Lean.Compiler.ConstFolding

@[inline]
abbrev Lean.Compiler.UnFoldFn :
Type
Equations
Equations
def Lean.Compiler.foldBinUInt (fn : Lean.Compiler.NumScalarTypeInfoBoolNatNatNat) (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) :
Equations
def Lean.Compiler.foldUIntAdd (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) :
Equations
def Lean.Compiler.foldUIntMul (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) :
Equations
def Lean.Compiler.foldUIntDiv (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) :
Equations
def Lean.Compiler.foldUIntMod (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) :
Equations
def Lean.Compiler.foldUIntSub (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) :
Equations
def Lean.Compiler.foldNatBinOp (fn : NatNatNat) (a₁ : Lean.Expr) (a₂ : Lean.Expr) :
Equations
Equations
def Lean.Compiler.toDecidableExpr (beforeErasure : Bool) (pred : Lean.Expr) (r : Bool) :
Equations
def Lean.Compiler.foldNatBinPred (mkPred : Lean.ExprLean.ExprLean.Expr) (fn : NatNatBool) (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) :
Equations
Equations
Equations
Equations
def Lean.Compiler.foldBinOp (beforeErasure : Bool) (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) :
Equations
def Lean.Compiler.foldUnOp (beforeErasure : Bool) (f : Lean.Expr) (a : Lean.Expr) :
Equations