Documentation

Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat

source
def Lean.Nat.fromExpr? (e : Expr) :
Meta.SimpM (Option Nat)
Instances For
    source
    def Nat.reduceSucc :
    Lean.Meta.Simp.DSimproc
    Instances For
      source
      def Nat.reduceAdd :
      Lean.Meta.Simp.DSimproc
      Instances For
        source
        def Nat.reduceMul :
        Lean.Meta.Simp.DSimproc
        Instances For
          source
          def Nat.reduceSub :
          Lean.Meta.Simp.DSimproc
          Instances For
            source
            def Nat.reduceDiv :
            Lean.Meta.Simp.DSimproc
            Instances For
              source
              def Nat.reduceMod :
              Lean.Meta.Simp.DSimproc
              Instances For
                source
                def Nat.reducePow :
                Lean.Meta.Simp.DSimproc
                Instances For
                  source
                  def Nat.reduceAnd :
                  Lean.Meta.Simp.DSimproc
                  Instances For
                    source
                    def Nat.reduceXor :
                    Lean.Meta.Simp.DSimproc
                    Instances For
                      source
                      def Nat.reduceOr :
                      Lean.Meta.Simp.DSimproc
                      Instances For
                        source
                        def Nat.reduceShiftLeft :
                        Lean.Meta.Simp.DSimproc
                        Instances For
                          source
                          def Nat.reduceShiftRight :
                          Lean.Meta.Simp.DSimproc
                          Instances For
                            source
                            def Nat.reduceGcd :
                            Lean.Meta.Simp.DSimproc
                            Instances For
                              source
                              def Nat.reduceLT :
                              Lean.Meta.Simp.Simproc
                              Instances For
                                source
                                def Nat.reduceGT :
                                Lean.Meta.Simp.Simproc
                                Instances For
                                  source
                                  def Nat.reduceBEq :
                                  Lean.Meta.Simp.DSimproc
                                  Instances For
                                    source
                                    def Nat.reduceBNe :
                                    Lean.Meta.Simp.DSimproc
                                    Instances For
                                      source
                                      def Nat.isValue :
                                      Lean.Meta.Simp.DSimproc

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

                                      Instances For
                                        source
                                        def Nat.reduceEqDiff :
                                        Lean.Meta.Simp.Simproc
                                        Instances For
                                          source
                                          def Nat.reduceBeqDiff :
                                          Lean.Meta.Simp.Simproc
                                          Instances For
                                            source
                                            def Nat.reduceBneDiff :
                                            Lean.Meta.Simp.Simproc
                                            Instances For
                                              source
                                              def Nat.reduceLeDiff :
                                              Lean.Meta.Simp.Simproc
                                              Instances For
                                                source
                                                def Nat.reduceSubDiff :
                                                Lean.Meta.Simp.Simproc
                                                Instances For
                                                  source
                                                  def Nat.reduceDvd :
                                                  Lean.Meta.Simp.Simproc
                                                  Instances For