structure Fin.Value : Type

• n : Nat
• value : Fin self.n

instance Fin.instDecidableEqValue : DecidableEq Fin.Value

instance Fin.instReprValue : Repr Fin.Value

Equations

• Fin.instReprValue = { reprPrec := Fin.reprValue✝ }

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

Equations

• Fin.fromExpr? e = do let __discr ← liftM (Lean.Meta.getFinValue? e) match __discr with | some ⟨n, value⟩ => pure (some { n := n, value := value }) | x => pure none

@[inline]

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

@[inline]

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

@[inline]

def Fin.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 Fin.reduceAdd : Lean.Meta.Simp.DSimproc

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

Equations

• Fin.reduceMul = Fin.reduceBin `HMul.hMul 6 fun {n : Nat} (x1 x2 : Fin n) => x1 * x2

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

Equations

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

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

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• Fin.reduceNe = Fin.reduceBinPred `Ne 3 fun (x1 x2 : Nat) => decide (x1 ≠ x2)

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

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

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

Simplification procedure for ensuring Fin n literals are normalized.

Equations

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

def Fin.reduceFinMk : Lean.Meta.Simp.DSimproc