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.etaStruct?.sameParams (params1 params2 : Array Expr) : MetaM Bool

def Lean.Meta.etaStruct?.getProjectedExpr (ctor induct : Name) (params : Array Expr) (idx : Nat) (e : Expr) (x? : Option Expr) : MetaM (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.

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.

partial def Lean.Meta.instantiateStructDefaultValueFn?.go? {m : Type → Type} [Monad m] [MonadLiftT MetaM m] (fieldVal? : Name → m (Option Expr)) (usedFields : NameSet) (e : Expr) : m (Option (NameSet × Expr))