structure Fin.Value : Type

• ofNatFn : Lean.Expr
• size : Nat
• value : Nat

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

Equations

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

def Fin.Value.toExpr (v : Fin.Value) : Lean.Expr

Equations

• Fin.Value.toExpr v = let vExpr := Lean.mkRawNatLit v.value; Lean.mkApp2 v.ofNatFn vExpr (Lean.mkApp2 (Lean.mkConst `Fin.instOfNat) (Lean.toExpr (v.size - 1)) vExpr)

@[inline]

def Fin.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 Fin.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.

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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