Documentation

Lean.Elab.DeclUtil

Equations
Instances For
    def Lean.Meta.forallTelescopeCompatible {m : TypeType u_1} {α : Type} [Monad m] [MonadControlT Lean.MetaM m] (type₁ : Lean.Expr) (type₂ : Lean.Expr) (numParams : Nat) (k : Array Lean.ExprLean.ExprLean.Exprm α) :
    m α

    Given two forall-expressions type₁ and type₂, ensure the first numParams parameters are compatible, and then execute k with the parameters and remaining types.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      Instances For
        Equations
        Instances For
          def Lean.Elab.sortDeclLevelParams (scopeParams : List Lake.Name) (allUserParams : List Lake.Name) (usedParams : Array Lake.Name) :

          Sort the given list of usedParams using the following order:

          • If it is an explicit level in allUserParams, then use user-given order.
          • All other levels come in lexicographic order after these.

          Remark: scopeParams are the universe params introduced using the universe command. allUserParams contains the universe params introduced using the universe command and the .{...} notation.

          Remark: this function return an exception if there is an u not in usedParams, that is in allUserParams but not in scopeParams.

          Remark: scopeParams and allUserParams are in reverse declaration order. That is, the head is the last declared parameter.

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