Documentation

Lean.Meta.Sym.Arith.Insts

Helpers for synthesizing the optional instances attached to a classified ring: IsCharP, PowIdentity, and NoNatZeroDivisors.

source
def Lean.Meta.Sym.Arith.getIsCharInst? (u : Level) (type semiringInst : Expr) :
SymM (Option (Expr × Nat))

Returns the IsCharP type semiringInst n instance together with the evaluated n.

Instances For
    source
    def Lean.Meta.Sym.Arith.getPowIdentityInst? (u : Level) (type : Expr) :
    SymM (Option (Expr × Expr × Nat))

    Returns the PowIdentity instance, the CommSemiring instance it was synthesized against, and the evaluated exponent p.

    Instances For
      source
      def Lean.Meta.Sym.Arith.getNoZeroDivInst? (u : Level) (type : Expr) :
      SymM (Option Expr)

      Returns the NoNatZeroDivisors instance for type, synthesizing the NatModule premise first.

      Instances For

        Order instances. Each returns none (with a debug issue) when synthInstance? fails.

        source
        def Lean.Meta.Sym.Arith.mkLawfulOrderLTInst? (u : Level) (type : Expr) (ltInst? leInst? : Option Expr) :
        SymM (Option Expr)
        Instances For
          source
          def Lean.Meta.Sym.Arith.mkIsPreorderInst? (u : Level) (type : Expr) (leInst? : Option Expr) :
          SymM (Option Expr)
          Instances For
            source
            def Lean.Meta.Sym.Arith.mkIsPartialOrderInst? (u : Level) (type : Expr) (leInst? : Option Expr) :
            SymM (Option Expr)
            Instances For
              source
              def Lean.Meta.Sym.Arith.mkIsLinearOrderInst? (u : Level) (type : Expr) (leInst? : Option Expr) :
              SymM (Option Expr)
              Instances For
                source
                def Lean.Meta.Sym.Arith.mkIsLinearPreorderInst? (u : Level) (type : Expr) (leInst? : Option Expr) :
                SymM (Option Expr)
                Instances For