Structure methods that require MetaM infrastructure

def Lean.Meta.getStructureName (struct : Expr) : MetaM Name

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.

structure Lean.Meta.StructProjDecl : Type

Structure projection declaration for mkProjections.

• ref : Syntax
• projName : Name
• paramInfoOverrides : List (Option BinderInfo)

  Overrides to param binders to apply after param binder info inference.

def Lean.Meta.mkProjections (n : Name) (projDecls : Array StructProjDecl) (instImplicit : Bool) : MetaM Unit

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.

def Lean.Meta.etaStruct? (e : Expr) (p : Name → Bool) : MetaM (Option Expr)

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.

def Lean.Meta.etaStructReduce (e : Expr) (p : Name → Bool) : MetaM Expr

Eta reduces all structures satisfying p in the whole expression.

See etaStruct? for reducing single expressions.

def Lean.Meta.instantiateStructDefaultValueFn? {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (defaultFn : Name) (levels? : Option (List Level)) (params : Array Expr) (fieldVal? : Name → m (Option Expr)) : m (Option (NameSet × 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.