def DocGen4.Process.withFields {α : Type} (info : Lean.InductiveVal) (k : Array (Lean.Name × Lean.Name × Lean.Expr) → Array (Lean.Name × Lean.Expr) → Lean.MetaM α) : Lean.MetaM α

Execute k with an array containing pairs (parentName, projFn, parentType) and an array containing pairs (fieldName, fieldType). k is executed in an updated local context which contains local declarations for the structName parameters.

Equations

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

partial def DocGen4.Process.getFieldOrigin (structName field : Lean.Name) : Lean.MetaM (Bool × Lean.Name)

Computes the origin of a field. Returns if the field was directly defined in this structure, and its projection function. Multiple parents could be the origin of a field, but we say the first parent that provides it is the one that determines the origin.

def DocGen4.Process.getFieldTypes (v : Lean.InductiveVal) : Lean.MetaM (Array StructureParentInfo × Array FieldInfo)

Equations

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

def DocGen4.Process.StructureInfo.ofInductiveVal (v : Lean.InductiveVal) : Lean.MetaM StructureInfo

Equations

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