Documentation

Lean.Meta.Sym.Arith.Functions

Cached function expressions for arithmetic operators #

Synthesizes and caches the canonical Lean expressions for arithmetic operators (+, *, -, ^, intCast, natCast, etc.). These cached expressions are used during reification to validate instances via pointer equality (isSameExpr).

Each getter checks the cache field first. On a miss, it synthesizes the instance, verifies it against the expected instance from the ring structure using isDefEqI, canonicalizes the result via canonExpr, and stores it.

source
def Lean.Meta.Sym.Arith.getNatSMulFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] :
m Expr
Instances For
    source
    def Lean.Meta.Sym.Arith.getIntSMulFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] :
    m Expr
    Instances For
      source
      def Lean.Meta.Sym.Arith.getAddFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
      m Expr
      Instances For
        source
        def Lean.Meta.Sym.Arith.getMulFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
        m Expr
        Instances For
          source
          def Lean.Meta.Sym.Arith.getSubFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
          m Expr
          Instances For
            source
            def Lean.Meta.Sym.Arith.getNegFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
            m Expr
            Instances For
              source
              def Lean.Meta.Sym.Arith.getPowFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
              m Expr
              Instances For
                source
                def Lean.Meta.Sym.Arith.getIntCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] :
                m Expr
                Instances For
                  source
                  def Lean.Meta.Sym.Arith.getNatCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] :
                  m Expr
                  Instances For
                    source
                    def Lean.Meta.Sym.Arith.getInvFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadCommRing m] :
                    m Expr
                    Instances For
                      source
                      def Lean.Meta.Sym.Arith.getDivFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadCommRing m] :
                      m Expr
                      Instances For
                        source
                        def Lean.Meta.Sym.Arith.getNatSMulFn' {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadSemiring m] :
                        m Expr
                        Instances For
                          source
                          def Lean.Meta.Sym.Arith.getAddFn' {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] :
                          m Expr
                          Instances For
                            source
                            def Lean.Meta.Sym.Arith.getMulFn' {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] :
                            m Expr
                            Instances For
                              source
                              def Lean.Meta.Sym.Arith.getPowFn' {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] :
                              m Expr
                              Instances For
                                source
                                def Lean.Meta.Sym.Arith.getNatCastFn' {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadSemiring m] :
                                m Expr
                                Instances For
                                  source
                                  def Lean.Meta.Sym.Arith.getToQFn {m : Type → Type} [Monad m] [MonadCanon m] [MonadCommSemiring m] :
                                  m Expr

                                  The embedding OfSemiring.toQ of the semiring into its envelope ring.

                                  Instances For
                                    source
                                    def Lean.Meta.Sym.Arith.getAddRightCancelInst? {m : Type → Type} [Monad m] [MonadCanon m] [MonadCommSemiring m] :
                                    m (Option Expr)

                                    The AddRightCancel instance of the semiring, if any. The result of the search is cached.

                                    Instances For