Lean.Elab.Structure

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

structure Lean.Elab.Command.ProjectionInfo :

Type

declName : Lean.Name
inferMod : Bool

source

structure Lean.Elab.Command.ElabStructResult :

Type

decl : Lean.Declaration
projInfos : List Lean.Elab.Command.ProjectionInfo
projInstances : List Lean.Name
mctx : Lean.MetavarContext
lctx : Lean.LocalContext
localInsts : Lean.LocalInstances
defaultAuxDecls : Array (Lean.Name × Lean.Expr × Lean.Expr)

source

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

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Command.checkValidFieldModifier modifiers = let _do_jp := fun y => let _do_jp := fun y => let _do_jp := fun y => if (Array.size modifiers.attrs != 0) = true then Lean.throwError (Lean.toMessageData "invalid use of attributes in field declaration") else pure PUnit.unit; if modifiers.isUnsafe = true then do let y ← Lean.throwError (Lean.toMessageData "invalid use of 'unsafe' in field declaration") _do_jp y else do let y ← pure PUnit.unit _do_jp y; if Lean.Elab.Modifiers.isPartial modifiers = true then do let y ← Lean.throwError (Lean.toMessageData "invalid use of 'partial' in field declaration") _do_jp y else do let y ← pure PUnit.unit _do_jp y; if modifiers.isNoncomputable = true then do let y ← Lean.throwError (Lean.toMessageData "invalid use of 'noncomputable' in field declaration") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

constant Lean.Elab.Command.structureDiamondWarning :

Lean.Option Bool

source

@[inline]

abbrev Lean.Elab.Command.FieldMap :

Type

Equations

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

source

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

Lean.Elab.Command.CommandElabM Unit

Equations

Lean.Elab.Command.elabStructure modifiers stx = do Lean.Elab.Command.checkValidInductiveModifier modifiers let isClass : Bool := Lean.Syntax.getKind (Lean.Syntax.getOp stx 0) == `Lean.Parser.Command.classTk let modifiers : Lean.Elab.Modifiers := if isClass = true then Lean.Elab.Modifiers.addAttribute modifiers { kind := Lean.AttributeKind.global, name := `class, stx := Lean.Syntax.missing } else modifiers let declId : Lean.Syntax := Lean.Syntax.getOp stx 1 let params : Array Lean.Syntax := Lean.Syntax.getArgs (Lean.Syntax.getOp stx 2) let exts : Lean.Syntax := Lean.Syntax.getOp stx 3 let parents : Array Lean.Syntax := if Lean.Syntax.isNone exts = true then #[] else Lean.Syntax.getSepArgs (Lean.Syntax.getOp (Lean.Syntax.getOp exts 0) 1) let optType : Lean.Syntax := Lean.Syntax.getOp stx 4 let derivingClassViews ← Lean.Elab.getOptDerivingClasses (Lean.Syntax.getOp stx 6) let _do_jp : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit := fun type => do let declName ← Lean.Elab.Command.runTermElabM none fun scopeVars => do let scopeLevelNames ← Lean.Elab.Term.getLevelNames let a ← Lean.getCurrNamespace let discr ← Lean.Elab.expandDeclId a scopeLevelNames declId modifiers let x : Lean.Elab.ExpandDeclIdResult := discr match x with | { shortName := name, declName := declName, levelNames := allUserLevelNames } => do Lean.Elab.addDeclarationRanges declName stx Lean.Elab.Term.withDeclName declName do let ctor ← Lean.Elab.Command.expandCtor stx modifiers declName let fields ← Lean.Elab.Command.expandFields stx modifiers declName Lean.Elab.Term.withLevelNames allUserLevelNames (Lean.Elab.Term.withAutoBoundImplicit (Lean.Elab.Term.elabBinders params fun params => do Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing false let params ← Lean.Elab.Term.addAutoBoundImplicits params let allUserLevelNames ← Lean.Elab.Term.getLevelNames Lean.Elab.Command.elabStructureView { ref := stx, modifiers := modifiers, scopeLevelNames := scopeLevelNames, allUserLevelNames := allUserLevelNames, isClass := isClass, declName := declName, scopeVars := scopeVars, params := params, parents := parents, type := type, ctor := ctor, fields := fields } let _do_jp : PUnit → Lean.Elab.TermElabM Lean.Name := fun y => pure declName if isClass = true then do let y ← pure PUnit.unit _do_jp y else do liftM (Lean.Meta.mkSizeOfInstances declName) let y ← liftM (Lean.Meta.mkInjectiveTheorems declName) _do_jp y)) Array.forM (fun view => Lean.Elab.DerivingClassView.applyHandlers view #[declName]) derivingClassViews 0 (Array.size derivingClassViews) if Lean.Syntax.isNone optType = true then do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.sort #[Lean.Syntax.atom info "Sort", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Level.hole #[Lean.Syntax.atom info "_"]]]) _do_jp y else do let y ← pure (Lean.Syntax.getOp (Lean.Syntax.getOp optType 0) 1) _do_jp y