def Nat.fromExpr? (e : Lean.Expr) : Lean.Meta.SimpM (Option Nat)

Equations

• Nat.fromExpr? e = liftM (Lean.Meta.getNatValue? e)

@[inline]

def Nat.reduceUnary (declName : Lean.Name) (arity : Nat) (op : Nat → Nat) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Equations

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

@[inline]

def Nat.reduceBin (declName : Lean.Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

@[inline]

def Nat.reduceBinPred (declName : Lean.Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

@[inline]

def Nat.reduceBoolPred (declName : Lean.Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Equations

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

def Nat.reduceSucc : Lean.Meta.Simp.DSimproc

Equations

• Nat.reduceSucc = Nat.reduceUnary `Nat.succ 1 fun (x : Nat) => x + 1

def Nat.reduceAdd : Lean.Meta.Simp.DSimproc

Equations

• Nat.reduceAdd = Nat.reduceBin `HAdd.hAdd 6 fun (x1 x2 : Nat) => x1 + x2

def Nat.reduceMul : Lean.Meta.Simp.DSimproc

def Nat.reduceSub : Lean.Meta.Simp.DSimproc

Equations

• Nat.reduceSub = Nat.reduceBin `HSub.hSub 6 fun (x1 x2 : Nat) => x1 - x2

def Nat.reduceDiv : Lean.Meta.Simp.DSimproc

Equations

• Nat.reduceDiv = Nat.reduceBin `HDiv.hDiv 6 fun (x1 x2 : Nat) => x1 / x2

def Nat.reduceMod : Lean.Meta.Simp.DSimproc

Equations

• Nat.reduceMod = Nat.reduceBin `HMod.hMod 6 fun (x1 x2 : Nat) => x1 % x2

def Nat.reducePow : Lean.Meta.Simp.DSimproc

Equations

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

def Nat.reduceAnd : Lean.Meta.Simp.DSimproc

def Nat.reduceXor : Lean.Meta.Simp.DSimproc

Equations

• Nat.reduceXor = Nat.reduceBin `HXor.hXor 6 fun (x1 x2 : Nat) => x1 ^^^ x2

def Nat.reduceOr : Lean.Meta.Simp.DSimproc

Equations

• Nat.reduceOr = Nat.reduceBin `HOr.hOr 6 fun (x1 x2 : Nat) => x1 ||| x2

def Nat.reduceShiftLeft : Lean.Meta.Simp.DSimproc

def Nat.reduceShiftRight : Lean.Meta.Simp.DSimproc

Equations

• Nat.reduceShiftRight = Nat.reduceBin `HShiftRight.hShiftRight 6 fun (x1 x2 : Nat) => x1 >>> x2

def Nat.reduceGcd : Lean.Meta.Simp.DSimproc

def Nat.reduceLT : Lean.Meta.Simp.Simproc

Equations

• Nat.reduceLT = Nat.reduceBinPred `LT.lt 4 fun (x1 x2 : Nat) => decide (x1 < x2)

def Nat.reduceGT : Lean.Meta.Simp.Simproc

Equations

• Nat.reduceGT = Nat.reduceBinPred `GT.gt 4 fun (x1 x2 : Nat) => decide (x1 > x2)

def Nat.reduceBEq : Lean.Meta.Simp.DSimproc

def Nat.reduceBNe : Lean.Meta.Simp.DSimproc

Equations

• Nat.reduceBNe = Nat.reduceBoolPred `bne 4 fun (x1 x2 : Nat) => x1 != x2

def Nat.isValue : Lean.Meta.Simp.DSimproc

Return .done for Nat values. We don't want to unfold in the symbolic evaluator.

Equations

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

def Nat.applySimprocConst (expr : Lean.Expr) (nm : Lean.Name) (args : Array Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

inductive Nat.EqResult : Type

• decide: Bool → Nat.EqResult
• false: Lean.Expr → Nat.EqResult
• eq: Lean.Expr → Lean.Expr → Lean.Expr → Nat.EqResult

def Nat.applyEqLemma (e : Lean.Expr → Nat.EqResult) (lemmaName : Lean.Name) (args : Array Lean.Expr) : Lean.Meta.SimpM (Option Nat.EqResult)

def Nat.reduceNatEqExpr (x y : Lean.Expr) : Lean.Meta.SimpM (Option Nat.EqResult)

Equations

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

def Nat.reduceEqDiff : Lean.Meta.Simp.Simproc

Equations

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

def Nat.reduceBeqDiff : Lean.Meta.Simp.Simproc

def Nat.reduceBneDiff : Lean.Meta.Simp.Simproc

def Nat.reduceLTLE (nm : Lean.Name) (arity : Nat) (isLT : Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

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

def Nat.reduceLeDiff : Lean.Meta.Simp.Simproc

def Nat.reduceSubDiff : Lean.Meta.Simp.Simproc