Constant folding for primitives that have special runtime support.

def Lean.Compiler.mkLcProof (p : Expr) : Expr

@[reducible, inline]

abbrev Lean.Compiler.BinFoldFn : Type

@[reducible, inline]

abbrev Lean.Compiler.UnFoldFn : Type

def Lean.Compiler.mkUIntTypeName (nbytes : Nat) : Name

structure Lean.Compiler.NumScalarTypeInfo : Type

• nbits : Nat
• id : Name
• ofNatFn : Name
• toNatFn : Name
• size : Nat

def Lean.Compiler.numScalarTypes : List NumScalarTypeInfo

def Lean.Compiler.isOfNat (fn : Name) : Bool

def Lean.Compiler.isToNat (fn : Name) : Bool

def Lean.Compiler.getInfoFromFn (fn : Name) : List NumScalarTypeInfo → Option NumScalarTypeInfo

def Lean.Compiler.getInfoFromVal : Expr → Option NumScalarTypeInfo

@[export lean_get_num_lit]

def Lean.Compiler.getNumLit : Expr → Option Nat

def Lean.Compiler.mkUIntLit (info : NumScalarTypeInfo) (n : Nat) : Expr

def Lean.Compiler.mkUInt32Lit (n : Nat) : Expr

def Lean.Compiler.foldBinUInt (fn : NumScalarTypeInfo → Bool → Nat → Nat → Nat) (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr

def Lean.Compiler.foldUIntAdd (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr

def Lean.Compiler.foldUIntMul (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr

def Lean.Compiler.foldUIntDiv (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr

def Lean.Compiler.foldUIntMod (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr

def Lean.Compiler.foldUIntSub (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr

def Lean.Compiler.preUIntBinFoldFns : List (Name × BinFoldFn)

def Lean.Compiler.uintBinFoldFns : List (Name × BinFoldFn)

def Lean.Compiler.foldNatBinOp (fn : Nat → Nat → Nat) (a₁ a₂ : Expr) : Option Expr

def Lean.Compiler.foldNatAdd : Bool → (a₁ a₂ : Expr) → Option Expr

def Lean.Compiler.foldNatMul : Bool → (a₁ a₂ : Expr) → Option Expr

def Lean.Compiler.foldNatDiv : Bool → (a₁ a₂ : Expr) → Option Expr

def Lean.Compiler.foldNatMod : Bool → (a₁ a₂ : Expr) → Option Expr

def Lean.Compiler.natPowThreshold : Nat

def Lean.Compiler.foldNatPow : Bool → (a₁ a₂ : Expr) → Option Expr

def Lean.Compiler.mkNatEq (a b : Expr) : Expr

def Lean.Compiler.mkNatLt (a b : Expr) : Expr

def Lean.Compiler.mkNatLe (a b : Expr) : Expr

def Lean.Compiler.toDecidableExpr (beforeErasure : Bool) (pred : Expr) (r : Bool) : Expr

def Lean.Compiler.foldNatBinPred (mkPred : Expr → Expr → Expr) (fn : Nat → Nat → Bool) (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr

def Lean.Compiler.foldNatDecEq (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr

def Lean.Compiler.foldNatDecLt (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr

def Lean.Compiler.foldNatDecLe (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr

def Lean.Compiler.foldNatBinBoolPred (fn : Nat → Nat → Bool) (a₁ a₂ : Expr) : Option Expr

def Lean.Compiler.foldNatBeq : Bool → (a₁ a₂ : Expr) → Option Expr

def Lean.Compiler.foldNatBlt : Bool → (a₁ a₂ : Expr) → Option Expr

def Lean.Compiler.foldNatBle : Bool → (a₁ a₂ : Expr) → Option Expr

def Lean.Compiler.natFoldFns : List (Name × BinFoldFn)

def Lean.Compiler.getBoolLit : Expr → Option Bool

def Lean.Compiler.foldStrictAnd : Bool → (a₁ a₂ : Expr) → Option Expr

def Lean.Compiler.foldStrictOr : Bool → (a₁ a₂ : Expr) → Option Expr

def Lean.Compiler.boolFoldFns : List (Name × BinFoldFn)

def Lean.Compiler.binFoldFns : List (Name × BinFoldFn)

def Lean.Compiler.foldNatSucc : Bool → (a : Expr) → Option Expr

def Lean.Compiler.foldCharOfNat (beforeErasure : Bool) (a : Expr) : Option Expr

def Lean.Compiler.foldToNat (size : Nat) : Bool → (a : Expr) → Option Expr

def Lean.Compiler.uintFoldToNatFns : List (Name × UnFoldFn)

def Lean.Compiler.unFoldFns : List (Name × UnFoldFn)

def Lean.Compiler.findBinFoldFn (fn : Name) : Option BinFoldFn

def Lean.Compiler.findUnFoldFn (fn : Name) : Option UnFoldFn

@[export lean_fold_bin_op]

def Lean.Compiler.foldBinOp (beforeErasure : Bool) (f a b : Expr) : Option Expr

@[export lean_fold_un_op]

def Lean.Compiler.foldUnOp (beforeErasure : Bool) (f a : Expr) : Option Expr