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