Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.Reify

source
def Lean.Meta.Grind.Arith.CommRing.isAddInst (inst : Expr) :
RingM Bool
Equations
Instances For
    source
    def Lean.Meta.Grind.Arith.CommRing.isMulInst (inst : Expr) :
    RingM Bool
    Equations
    Instances For
      source
      def Lean.Meta.Grind.Arith.CommRing.isSubInst (inst : Expr) :
      RingM Bool
      Equations
      Instances For
        source
        def Lean.Meta.Grind.Arith.CommRing.isNegInst (inst : Expr) :
        RingM Bool
        Equations
        Instances For
          source
          def Lean.Meta.Grind.Arith.CommRing.isPowInst (inst : Expr) :
          RingM Bool
          Equations
          Instances For
            source
            def Lean.Meta.Grind.Arith.CommRing.isIntCastInst (inst : Expr) :
            RingM Bool
            Equations
            Instances For
              source
              def Lean.Meta.Grind.Arith.CommRing.isNatCastInst (inst : Expr) :
              RingM Bool
              Equations
              Instances For
                source
                def Lean.Meta.Grind.Arith.CommRing.reify? (e : Expr) (skipVar : Bool := true) (gen : Nat := 0) :
                RingM (Option RingExpr)

                Converts a Lean expression e in the CommRing into a CommRing.Expr object.

                If skipVar is true, then the result is none if e is not an interpreted CommRing term. We use skipVar := false when processing inequalities, and skipVar := true for equalities and disequalities

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Lean.Meta.Grind.Arith.CommRing.sreify? (e : Expr) :
                  SemiringM (Option SemiringExpr)

                  Similar to reify? but for CommSemiring

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