Documentation

Lean.Elab.Structure

structure Lean.Elab.Command.StructCtorView:

Type

ref : Lean.Syntax
modifiers : Lean.Elab.Modifiers
name : Lean.Name
declName : Lean.Name

structure Lean.Elab.Command.StructFieldView:

Type

ref : Lean.Syntax
modifiers : Lean.Elab.Modifiers
binderInfo : Lean.BinderInfo
declName : Lean.Name
name : Lean.Name
rawName : Lean.Name
binders : Lean.Syntax
type? : Option Lean.Syntax
value? : Option Lean.Syntax

structure Lean.Elab.Command.StructView:

Type

ref : Lean.Syntax
modifiers : Lean.Elab.Modifiers
scopeLevelNames : List Lean.Name
allUserLevelNames : List Lean.Name
isClass : Bool
declName : Lean.Name
scopeVars : Array Lean.Expr
params : Array Lean.Expr
parents : Array Lean.Syntax
type : Lean.Syntax
ctor : Lean.Elab.Command.StructCtorView
fields : Array Lean.Elab.Command.StructFieldView

inductive Lean.Elab.Command.StructFieldKind:

Type

newField: Lean.Elab.Command.StructFieldKind
copiedField: Lean.Elab.Command.StructFieldKind
fromParent: Lean.Elab.Command.StructFieldKind
subobject: Lean.Elab.Command.StructFieldKind

instance Lean.Elab.Command.instInhabitedStructFieldKind:

Inhabited Lean.Elab.Command.StructFieldKind

Equations

Lean.Elab.Command.instInhabitedStructFieldKind = { default := Lean.Elab.Command.StructFieldKind.newField }

instance Lean.Elab.Command.instDecidableEqStructFieldKind:

DecidableEq Lean.Elab.Command.StructFieldKind

Equations

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

instance Lean.Elab.Command.instReprStructFieldKind:

Repr Lean.Elab.Command.StructFieldKind

Equations

Lean.Elab.Command.instReprStructFieldKind = { reprPrec := [anonymous] }

structure Lean.Elab.Command.StructFieldInfo:

Type

name : Lean.Name
declName : Lean.Name
fvar : Lean.Expr
kind : Lean.Elab.Command.StructFieldKind
value? : Option Lean.Expr

instance Lean.Elab.Command.instInhabitedStructFieldInfo:

Inhabited Lean.Elab.Command.StructFieldInfo

Equations

Lean.Elab.Command.instInhabitedStructFieldInfo = { default := { name := default, declName := default, fvar := default, kind := default, value? := default } }

instance Lean.Elab.Command.instReprStructFieldInfo:

Repr Lean.Elab.Command.StructFieldInfo

Equations

Lean.Elab.Command.instReprStructFieldInfo = { reprPrec := [anonymous] }

def Lean.Elab.Command.StructFieldInfo.isFromParent (info : Lean.Elab.Command.StructFieldInfo) :

Equations

Lean.Elab.Command.StructFieldInfo.isFromParent info = match info.kind with | Lean.Elab.Command.StructFieldKind.fromParent => true | x => false

def Lean.Elab.Command.StructFieldInfo.isSubobject (info : Lean.Elab.Command.StructFieldInfo) :

Equations

Lean.Elab.Command.StructFieldInfo.isSubobject info = match info.kind with | Lean.Elab.Command.StructFieldKind.subobject => true | x => false

structure Lean.Elab.Command.ElabStructResult:

Type (u_1 + 1)

decl : Lean.Declaration
projInfos : {ProjectionInfo : Type u_1} → List ProjectionInfo
projInstances : List Lean.Name
mctx : Lean.MetavarContext
lctx : Lean.LocalContext
localInsts : Lean.LocalInstances
defaultAuxDecls : Array (Lean.Name × Lean.Expr × Lean.Expr)

def Lean.Elab.Command.checkValidFieldModifier (modifiers : Lean.Elab.Modifiers) :

Lean.Elab.TermElabM Unit

Equations

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

opaque Lean.Elab.Command.structureDiamondWarning:

Lean.Option Bool

@[inline]

abbrev Lean.Elab.Command.FieldMap:

Type

Equations

Lean.Elab.Command.FieldMap = Lean.NameMap Lean.Expr

def Lean.Elab.Command.elabStructure (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) :

Lean.Elab.Command.CommandElabM Unit

Equations

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