structure Fin.Value : Type

• n : Nat
• value : Fin self.n

@[implicit_reducible]

instance Fin.instDecidableEqValue : DecidableEq Value

def Fin.instDecidableEqValue.decEq (x✝ x✝¹ : Value) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Fin.instReprValue : Repr Value

def Fin.instReprValue.repr : Value → Nat → Std.Format

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

@[inline]

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

@[inline]

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

@[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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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