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.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.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