Deriving handlers

• deriving FromRow decodes a row into a structure, reading each field from the query variable of the same name (Option fields are optional columns).
• deriving Entity / deriving Relation map a structure to a TypeDB type (TypeDB.ORM.Mapped), and add Keyed when a field is a Key, and S.field.<name> handles for its attribute fields.
• deriving Polymorphic decodes a sum of mapped types by each instance's concrete type.

The generated code types every field through its projection (fun (x : S) => x.f), so it never spells out a field's type.

structure TypeDB.Deriving.Markers : Type

What a field's declared type says through the Key, Role and Attr markers.

• key : Bool
• role : Option String
• label : Option String

@[instance_reducible]

instance TypeDB.Deriving.instInhabitedMarkers : Inhabited Markers

Equations

• TypeDB.Deriving.instInhabitedMarkers = { default := TypeDB.Deriving.instInhabitedMarkers.default }

partial def TypeDB.Deriving.markers (t : Lean.Expr) : Markers

structure TypeDB.Deriving.FieldInfo : Type

A flattened field of a structure.

• name : Lean.Name
• markers : Markers
• inherited : Bool

  Declared in a parent structure that is itself mapped.

@[instance_reducible]

instance TypeDB.Deriving.instInhabitedFieldInfo : Inhabited FieldInfo

Equations

• TypeDB.Deriving.instInhabitedFieldInfo = { default := TypeDB.Deriving.instInhabitedFieldInfo.default }

def TypeDB.Deriving.fieldInfos (s : Lean.Name) : Lean.Elab.TermElabM (Array FieldInfo)

Equations

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

FromRow

def TypeDB.Deriving.mkFromRow (s : Lean.Name) : Lean.Elab.TermElabM Lean.Command

Equations

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

def TypeDB.Deriving.fromRowHandler (names : Array Lean.Name) : Lean.Elab.Command.CommandElabM Bool

Equations

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

Entity and Relation

def TypeDB.Deriving.mkMapped (s : Lean.Name) (kind : ORM.Kind) : Lean.Elab.TermElabM (Array Lean.Command)

Equations

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

def TypeDB.Deriving.mappedHandler (kind : ORM.Kind) (names : Array Lean.Name) : Lean.Elab.Command.CommandElabM Bool

Equations

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

Polymorphic

def TypeDB.Deriving.mkPolymorphic (t : Lean.Name) : Lean.Elab.TermElabM Lean.Command

Equations

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

def TypeDB.Deriving.polymorphicHandler (names : Array Lean.Name) : Lean.Elab.Command.CommandElabM Bool

Equations

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