Documentation

Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin

structure Fin.Value :
Instances For
    Equations
      Instances For
        @[inline]
        def Fin.reduceOp (declName : Lean.Name) (arity : Nat) (f : NatNat) (op : {n : Nat} → Fin nFin (f n)) (e : Lean.Expr) :
        Equations
          Instances For
            @[inline]
            def Fin.reduceNatOp (declName : Lean.Name) (arity : Nat) (f : NatNat) (op : (n : Nat) → Fin (f n)) (e : Lean.Expr) :
            Equations
              Instances For
                @[inline]
                def Fin.reduceBin (declName : Lean.Name) (arity : Nat) (op : {n : Nat} → Fin nFin nFin n) (e : Lean.Expr) :
                Equations
                  Instances For
                    @[inline]
                    def Fin.reduceBinPred (declName : Lean.Name) (arity : Nat) (op : NatNatBool) (e : Lean.Expr) :
                    Equations
                      Instances For
                        @[inline]
                        def Fin.reduceBoolPred (declName : Lean.Name) (arity : Nat) (op : NatNatBool) (e : Lean.Expr) :
                        Equations
                          Instances For
                            Equations
                              Instances For
                                Equations
                                  Instances For
                                    Equations
                                      Instances For
                                        Equations
                                          Instances For
                                            Equations
                                              Instances For
                                                Equations
                                                  Instances For
                                                    Equations
                                                      Instances For
                                                        Equations
                                                          Instances For
                                                            Equations
                                                              Instances For
                                                                Equations
                                                                  Instances For
                                                                    Equations
                                                                      Instances For
                                                                        Equations
                                                                          Instances For
                                                                            Equations
                                                                              Instances For
                                                                                Equations
                                                                                  Instances For
                                                                                    Equations
                                                                                      Instances For
                                                                                        Equations
                                                                                          Instances For
                                                                                            Equations
                                                                                              Instances For

                                                                                                Simplification procedure for ensuring Fin n literals are normalized.

                                                                                                Equations
                                                                                                  Instances For