Documentation

Mathlib.Tactic.Inclusion.ExtensionAPI.Basic

Basic API for inclusion extensions #

This file defines helpers for safely interacting with the InclusionM and HypothesisM monads when constructing extensions for the inclusion tactic.

source
def Inclusion.InclusionM.getParam? (name : Lean.Name) :
InclusionM (Option Lean.Expr)

Return the value of parameter name, if it was supplied or has a default.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Inclusion.InclusionM.getParam (name : Lean.Name) :
    InclusionM Lean.Expr

    Return the value of parameter name.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Inclusion.HypothesisM.getParam? (name : Lean.Name) :
      HypothesisM (Option Lean.Expr)

      Return the value of parameter name, if it was supplied or has a default.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Inclusion.HypothesisM.getParam (name : Lean.Name) :
        HypothesisM Lean.Expr

        Return the value of parameter name, or report that it was not supplied.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Inclusion.delabIVarDisplay :
          Lean.PrettyPrinter.Delaborator.Delab

          Delaborate an inclusion set variable as I[e].

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Inclusion.mkIVar (iExpr : IExpr) (cover? : Option Lean.Expr := none) :
            InclusionM IVar

            Create and register an inclusion variable for iExpr.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Inclusion.mkNDIVarExt (family : Lean.Name) (iType : IType) (mkCover? : InclusionM (Option Lean.Expr) := pure none) (priority : ℕ := 100) (name : Lean.Name := by exact decl_name%) :
              InclusionExt

              Construct an inclusion extension for making non dependently typed inclusion variables.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Inclusion.findIVar? (e : Lean.Expr) :
                HypothesisM (Option IVar)

                Return the inclusion variable registered for e, if there is one.

                Equations
                Instances For
                  source
                  def Inclusion.ensureOutputType (type expectedType : IType) :
                  Lean.MetaM Unit

                  Check that two inclusion types are definitionally equal, including their chosen ToSet instances.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Inclusion.mkHypExprInclusionBody (e : Lean.Expr) :
                    HypothesisM ExprInclusionBody

                    Construct a closed inclusion body for an expression argument of a hypothesis rule.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Inclusion.addInclusionHyp (iExpr : IExpr) (body : ExprInclusionBody) :
                      HypothesisM Unit

                      Add the inclusion hypothesis body for iExpr.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For