structure Fin.Value : Type

• n : Nat
• value : Fin self.n

instance Fin.instDecidableEqValue : DecidableEq Value

Equations

• Fin.instDecidableEqValue = Fin.decEqValue✝

instance Fin.instReprValue : Repr Value

Equations

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

def Fin.fromExpr? (e : Lean.Expr) : Lean.Meta.SimpM (Option 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.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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

def Fin.reduceBinPred (declName : Lean.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 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.reduceSucc : Lean.Meta.Simp.DSimproc

Equations

• Fin.reduceSucc = Fin.reduceOp `Fin.succ 2 (fun (x : Nat) => x + 1) fun {n : Nat} => Fin.succ

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

Equations

• Fin.reduceRev = Fin.reduceOp `Fin.rev 2 (fun (x : Nat) => x) fun {n : Nat} => Fin.rev

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

Equations

• Fin.reduceLast = Fin.reduceNatOp `Fin.last 1 (fun (x : Nat) => x + 1) Fin.last

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Fin.reduceAnd = Fin.reduceBin `HAnd.hAnd 6 fun {n : Nat} (x1 x2 : Fin n) => x1 &&& x2

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

Equations

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

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

Equations

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

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

Equations

• Fin.reduceShiftLeft = Fin.reduceBin `HShiftLeft.hShiftLeft 6 fun {n : Nat} (x1 x2 : Fin n) => x1 <<< x2

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

Equations

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

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

Equations

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

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

Equations

• Fin.reduceEq = Fin.reduceBinPred `Eq 3 fun (x1 x2 : Nat) => decide (x1 = x2)

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

Equations

• Fin.reduceBEq = Fin.reduceBoolPred `BEq.beq 4 fun (x1 x2 : Nat) => x1 == x2

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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