Documentation

Lean.Meta.Structure

Structure methods that require MetaM infrastructure #

If struct is an application of the form S .. with S a constant for a structure, returns the name of the structure, otherwise throws an error.

Equations
    Instances For

      Structure projection declaration for mkProjections.

      Instances For
        def Lean.Meta.mkProjections (n : Name) (projDecls : Array StructProjDecl) (instImplicit : Bool) :

        Adds projection functions to the environment for the one-constructor inductive type named n.

        • The projNames in each StructProjDecl are used for the names of the declarations added to the environment.
        • If instImplicit is true, then generates projections with self being instance implicit.

        Notes:

        • This function supports everything that Expr.proj supports (see lean::type_checker::infer_proj). This means we can generate projections for inductive types with one-constructor, even if it is an indexed family (which is not supported by the structure command).
        • We throw errors in the cases that Expr.proj is not type-correct.
        Equations
          Instances For

            Checks if the expression is of the form S.mk x.1 ... x.n with n nonzero and S.mk a structure constructor with S one of the recorded structure parents. Returns x. Each projection x.i can be either a native projection or from a projection function.

            Equations
              Instances For
                Equations
                  Instances For
                    def Lean.Meta.etaStruct?.getProjectedExpr (ctor induct : Name) (params : Array Expr) (idx : Nat) (e : Expr) (x? : Option Expr) :

                    Given an expression e that's either a native projection or a registered projection function, gives the object being projected. Checks that the parameters are defeq to params, that the projection index is equal to idx, and, if x? is provided, that the object being projected is equal to it.

                    Equations
                      Instances For

                        Eta reduces all structures satisfying p in the whole expression.

                        See etaStruct? for reducing single expressions.

                        Equations
                          Instances For
                            def Lean.Meta.instantiateStructDefaultValueFn? {m : TypeType} [Monad m] [MonadEnv m] [MonadError m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (defaultFn : Name) (levels? : Option (List Level)) (params : Array Expr) (fieldVal? : Namem (Option Expr)) :

                            Instantiates the default value given by the default value function defaultFn.

                            • defaultFn is the default value function returned by Lean.getEffectiveDefaultFnForField? or Lean.getDefaultFnForField?.
                            • levels? is the list of levels to use, and otherwise the levels are inferred.
                            • params is the list of structure parameters. These are assumed to be correct for the given levels.
                            • fieldVal? is a function for getting fields for values, if they exist.

                            If successful, returns a set of fields used and the resulting default value. Success is expected. Callers should do metacontext backtracking themselves if needed.

                            Equations
                              Instances For
                                partial def Lean.Meta.instantiateStructDefaultValueFn?.go? {m : TypeType} [Monad m] [MonadLiftT MetaM m] (fieldVal? : Namem (Option Expr)) (usedFields : NameSet) (e : Expr) :