Documentation

Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int

Equations
    Instances For
      @[inline]
      def Int.reduceUnary (declName : Lean.Name) (arity : Nat) (op : IntInt) (e : Lean.Expr) :
      Equations
        Instances For
          @[inline]
          def Int.reduceBin (declName : Lean.Name) (arity : Nat) (op : IntIntInt) (e : Lean.Expr) :
          Equations
            Instances For
              Equations
                Instances For
                  @[inline]
                  def Int.reduceBinPred (declName : Lean.Name) (arity : Nat) (op : IntIntBool) (e : Lean.Expr) :
                  Equations
                    Instances For
                      @[inline]
                      def Int.reduceBoolPred (declName : Lean.Name) (arity : Nat) (op : IntIntBool) (e : Lean.Expr) :
                      Equations
                        Instances For
                          Equations
                            Instances For

                              Return .done for positive Int values. We don't want to unfold in the symbolic evaluator.

                              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
                                                                                          @[inline]
                                                                                          Equations
                                                                                            Instances For
                                                                                              Equations
                                                                                                Instances For
                                                                                                  Equations
                                                                                                    Instances For