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.

Equations

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

structure Lean.Meta.StructProjDecl : Type

Structure projection declaration for mkProjections.

• ref : Syntax
• projName : Name

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.

Equations

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