Records

Record fields is both the index of a record-sorted term and the Lean value such a term denotes, fields being its named fields in order. The order is part of the sort: {a : Int, b : Bool} and {b : Bool, a : Int} are different sorts.

def origin : Record [("x", Int), ("y", Int)] := .cons "x" 0 (.last "y" 0)
#eval origin.get "y"   -- 0

class Cvc.ToTypFields (fields : List (String × Type)) : Type

The Typs a list of named Lean types denotes.

• typs : List (String × Typ)

  The fields, in order, at their Typs.

@[instance_reducible]

instance Cvc.ToTypFields.instNilProdStringType : ToTypFields []

Equations

• Cvc.ToTypFields.instNilProdStringType = { typs := [] }

@[instance_reducible]

instance Cvc.ToTypFields.instConsProdStringTypeMkOfToTyp {α : Type} {fields : List (String × Type)} {name : String} [A : ToTyp α] [Fs : ToTypFields fields] : ToTypFields ((name, α) :: fields)

Equations

• Cvc.ToTypFields.instConsProdStringTypeMkOfToTyp = { typs := (name, Cvc.ToTyp.typ α) :: Cvc.ToTypFields.typs fields }

def Cvc.Values : List (String × Type) → Type

A record's field values: gamma for each field, in order, as nested pairs ending in PUnit.

Equations

• Cvc.Values [] = PUnit
• Cvc.Values ((_name, gamma) :: rest) = (gamma × Cvc.Values rest)

structure Cvc.Record (fields : List (String × Type)) : Type

A record of the named, ordered fields: a record sort, and a value of it.

• values : Values fields

  The field values, in order.

def Cvc.Record.last {gamma : Type} (_name : String) (value : gamma) : Record [(_name, gamma)]

A record's last field, and its value.

Equations

• Cvc.Record.last _name value = { values := (value, PUnit.unit) }

def Cvc.Record.cons {gamma : Type} {fields : List (String × Type)} (_name : String) (value : gamma) (rest : Record fields) : Record ((_name, gamma) :: fields)

Adds a field's value in front of the ones collected so far.

Equations

• Cvc.Record.cons _name value rest = { values := (value, rest.values) }

class Cvc.FieldOf (fields : List (String × Type)) (name : String) (gamma : outParam Type) : Type

name is one of fields, with type gamma: where it sits, and how to reach it.

Resolved by instance search, so a name that is not a field, or one asked for at the wrong type, does not compile.

• idx : Fin fields.length

  Where the field sits in fields.

• get : Values fields → gamma

  The field's value.

• set : Values fields → gamma → Values fields

  The values, with this field's replaced.

@[instance_reducible, instance 10000]

instance Cvc.instFieldOfConsProdStringTypeMk {name : String} {gamma : Type} {fields : List (String × Type)} : FieldOf ((name, gamma) :: fields) name gamma

Equations

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

@[instance_reducible]

instance Cvc.instFieldOfConsProdStringTypeMk_1 {fields : List (String × Type)} {name : String} {gamma : Type} {_other : String} {_beta : Type} [F : FieldOf fields name gamma] : FieldOf ((_other, _beta) :: fields) name gamma

Equations

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

def Cvc.Record.get {fields : List (String × Type)} (r : Record fields) {gamma : Type} (name : String) [F : FieldOf fields name gamma] : gamma

A field's value.

Total: a name that is not a field has no FieldOf instance, so there is no none to answer.

Equations

• r.get name = Cvc.FieldOf.get name r.values

def Cvc.Record.set {fields : List (String × Type)} (r : Record fields) {gamma : Type} (name : String) [F : FieldOf fields name gamma] (value : gamma) : Record fields

The same record, with one field's value replaced.

Equations

• r.set name value = { values := Cvc.FieldOf.set name r.values value }

Instances for nesting

A record's order, equality, hash and string form are lifted field by field, each through its own class, so a record demands of its fields only what is asked of the record.

class Cvc.OrdFields (fields : List (String × Type)) : Type

Lifts Ord over a record's fields, lexicographically.

• compare : Values fields → Values fields → Ordering

  Compares two records' values.

@[instance_reducible]

instance Cvc.instOrdFieldsNilProdStringType : OrdFields []

Equations

• Cvc.instOrdFieldsNilProdStringType = { compare := fun (x x_1 : Cvc.Values []) => Ordering.eq }

@[instance_reducible]

instance Cvc.instOrdFieldsConsProdStringTypeMkOfOrd {gamma : Type} {fields : List (String × Type)} {_name : String} [Ord gamma] [R : OrdFields fields] : OrdFields ((_name, gamma) :: fields)

Equations

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

class Cvc.DecidableEqFields (fields : List (String × Type)) : Type

Lifts DecidableEq over a record's fields.

• decEq : DecidableEq (Values fields)

  Decides equality of two records' values.

@[instance_reducible]

instance Cvc.instDecidableEqFieldsNilProdStringType : DecidableEqFields []

Equations

• Cvc.instDecidableEqFieldsNilProdStringType = { decEq := fun (x x_1 : Cvc.Values []) => isTrue ⋯ }

@[instance_reducible]

instance Cvc.instDecidableEqFieldsConsProdStringTypeMkOfDecidableEq {gamma : Type} {fields : List (String × Type)} {_name : String} [DecidableEq gamma] [R : DecidableEqFields fields] : DecidableEqFields ((_name, gamma) :: fields)

Equations

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

class Cvc.HashableFields (fields : List (String × Type)) : Type

Lifts Hashable over a record's fields.

• hash : Values fields → UInt64

  Hashes a record's values.

@[instance_reducible]

instance Cvc.instHashableFieldsNilProdStringType : HashableFields []

Equations

• Cvc.instHashableFieldsNilProdStringType = { hash := fun (x : Cvc.Values []) => 0 }

@[instance_reducible]

instance Cvc.instHashableFieldsConsProdStringTypeMkOfHashable {gamma : Type} {fields : List (String × Type)} {_name : String} [Hashable gamma] [R : HashableFields fields] : HashableFields ((_name, gamma) :: fields)

Equations

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

class Cvc.ToStringFields (fields : List (String × Type)) : Type

Lifts ToString over a record's fields, and names them.

• strings : Values fields → List String

  One name := value per field, in order.

@[instance_reducible]

instance Cvc.instToStringFieldsNilProdStringType : ToStringFields []

Equations

• Cvc.instToStringFieldsNilProdStringType = { strings := fun (x : Cvc.Values []) => [] }

@[instance_reducible]

instance Cvc.instToStringFieldsConsProdStringTypeMkOfToString {gamma : Type} {fields : List (String × Type)} {name : String} [ToString gamma] [R : ToStringFields fields] : ToStringFields ((name, gamma) :: fields)

Equations

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

@[instance_reducible]

instance Cvc.instOrdRecordOfOrdFields {fields : List (String × Type)} [O : OrdFields fields] : Ord (Record fields)

Equations

• Cvc.instOrdRecordOfOrdFields = { compare := fun (a b : Cvc.Record fields) => Cvc.OrdFields.compare a.values b.values }

@[instance_reducible]

instance Cvc.instDecidableEqRecordOfDecidableEqFields {fields : List (String × Type)} [D : DecidableEqFields fields] : DecidableEq (Record fields)

Equations

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

@[instance_reducible]

instance Cvc.instHashableRecordOfHashableFields {fields : List (String × Type)} [H : HashableFields fields] : Hashable (Record fields)

Equations

• Cvc.instHashableRecordOfHashableFields = { hash := fun (r : Cvc.Record fields) => Cvc.HashableFields.hash r.values }

@[instance_reducible]

instance Cvc.instToStringRecordOfToStringFields {fields : List (String × Type)} [S : ToStringFields fields] : ToString (Record fields)

Equations

• Cvc.instToStringRecordOfToStringFields = { toString := fun (r : Cvc.Record fields) => "{" ++ ", ".intercalate (Cvc.ToStringFields.strings r.values) ++ "}" }

@[instance_reducible]

instance Cvc.instToTypRecordOfToTypFields {fields : List (String × Type)} [Fs : ToTypFields fields] : ToTyp (Record fields)

Equations

• Cvc.instToTypRecordOfToTypFields = { typ := Cvc.Typ.record (Cvc.ToTypFields.typs fields) }