Documentation

Lean.Meta.Sym.ProofInstInfo

source
def Lean.Meta.Sym.preprocessType (type : Expr) (zetaReduceLHSOnly zetaDelta : Bool := false) :
MetaM Expr

Preprocesses types that used for pattern matching and unification.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Meta.Sym.mkProofInstArgInfo? (xs : Array Expr) :
    MetaM (Option ProofInstInfo)

    Analyzes whether the given free variables (aka arguments) are proofs or instances. Returns none if no arguments are proofs or instances.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Meta.Sym.mkProofInstInfo? (declName : Name) :
      MetaM (Option ProofInstInfo)

      Analyzes the type signature of declName and returns information about which arguments are proofs or instances. Returns none if no arguments are proofs or instances.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Meta.Sym.getProofInstInfo? (declName : Name) :
        SymM (Option ProofInstInfo)

        Returns information about the type signature of declName. It contains information about which arguments are proofs or instances. Returns none if no arguments are proofs or instances.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Meta.Sym.getProofInstInfoOfFVar? (fvarId : FVarId) :
          SymM (Option ProofInstInfo)

          Returns information about the type of the local declaration fvarId. It contains information about which arguments are proofs or instances. Returns none if no arguments are proofs or instances.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Meta.Sym.getProofInstInfoOfExpr? (e : Expr) :
            SymM (Option ProofInstInfo)

            Returns information about which arguments of the function e are proofs or instances, see getProofInstInfo? and getProofInstInfoOfFVar?. Returns none if e is neither a constant nor a local declaration.

            Equations
            Instances For