Documentation

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

source
def Lean.Meta.Grind.Arith.CommRing.isAddInst (ring : Ring) (inst : Expr) :
Bool
Equations
Instances For
    source
    def Lean.Meta.Grind.Arith.CommRing.isMulInst (ring : Ring) (inst : Expr) :
    Bool
    Equations
    Instances For
      source
      def Lean.Meta.Grind.Arith.CommRing.isSubInst (ring : Ring) (inst : Expr) :
      Bool
      Equations
      Instances For
        source
        def Lean.Meta.Grind.Arith.CommRing.isNegInst (ring : Ring) (inst : Expr) :
        Bool
        Equations
        Instances For
          source
          def Lean.Meta.Grind.Arith.CommRing.isPowInst (ring : Ring) (inst : Expr) :
          Bool
          Equations
          Instances For
            source
            def Lean.Meta.Grind.Arith.CommRing.isIntCastInst (ring : Ring) (inst : Expr) :
            Bool
            Equations
            Instances For
              source
              def Lean.Meta.Grind.Arith.CommRing.isNatCastInst (ring : Ring) (inst : Expr) :
              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
                  partial def Lean.Meta.Grind.Arith.CommRing.reify?.go (toVar asVar : Expr → RingM RingExpr) (e : Expr) :
                  RingM RingExpr
                  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
                    source
                    partial def Lean.Meta.Grind.Arith.CommRing.sreify?.go (toVar asVar : Expr → SemiringM SemiringExpr) (e : Expr) :
                    SemiringM SemiringExpr