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 : Lake.Name) (arity : Nat) (op : Nat → Nat) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Nat.reduceBoolPred (declName : Lake.Name) (arity : Nat) (op : Nat → Nat → 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.reduceSucc : Lean.Meta.Simp.Simproc

Equations

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

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

Equations

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

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

Equations

• Nat.reduceMul = Nat.reduceBin `HMul.hMul 6 fun (x x_1 : Nat) => x * x_1

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Nat.reducePow = Nat.reduceBin `HPow.hPow 6 fun (x x_1 : Nat) => x ^ x_1

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

Equations

• Nat.reduceGcd = Nat.reduceBin `Nat.gcd 2 Nat.gcd

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

Equations

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

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

Equations

• Nat.reduceLE = Nat.reduceBinPred `LE.le 4 fun (x x_1 : Nat) => decide (x ≤ x_1)

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

Equations

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

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

Equations

• Nat.reduceGE = Nat.reduceBinPred `GE.ge 4 fun (x x_1 : Nat) => decide (x ≥ x_1)

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

Equations

• Nat.reduceEq = Nat.reduceBinPred `Eq 3 fun (x x_1 : Nat) => decide (x = x_1)

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

Equations

• Nat.reduceNe = Nat.reduceBinPred `Ne 3 fun (x x_1 : Nat) => decide (x ≠ x_1)

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

Equations

• Nat.reduceBEq = Nat.reduceBoolPred `BEq.beq 4 fun (x x_1 : Nat) => x == x_1

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

Equations

• Nat.reduceBNe = Nat.reduceBoolPred `bne 4 fun (x x_1 : Nat) => x != x_1

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

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.