Data.Record

An ordered record is a record whose field names have to appear in
a fixed order, but must otherwise be distinct.

Reexports

Definitions

ArgList : Type

Totality: total
Visibility: public export

Field : (String -> Type) -> Type

Totality: total
Visibility: public export

Fields : (String -> Type) -> Type

Totality: total
Visibility: public export

record Record : {0 A : String -> Type} -> (0 _ : (Field A -> Type)) -> (0 _ : Fields A) -> Type

Totality: total
Visibility: public export
Constructor: 

MkRecord : {0 A : String -> Type} -> {0 F : Field A -> Type} -> {0 Flds : Fields A} -> All F Flds -> Record F Flds

Projection: 

.content : {0 A : String -> Type} -> {0 F : Field A -> Type} -> {0 Flds : Fields A} -> Record F Flds -> All F Flds

.content : {0 A : String -> Type} -> {0 F : Field A -> Type} -> {0 Flds : Fields A} -> Record F Flds -> All F Flds

Totality: total
Visibility: public export

content : {0 A : String -> Type} -> {0 F : Field A -> Type} -> {0 Flds : Fields A} -> Record F Flds -> All F Flds

Totality: total
Visibility: public export

map : ((x : Field a) -> f x -> g x) -> Record f flds -> Record g flds

Totality: total
Visibility: public export

IsField : String -> Fields a -> Type

Totality: total
Visibility: public export

isYesBecause : (d : Dec p) -> p -> IsYes d

Totality: total
Visibility: public export

soNotToEq : So (not b) -> b = False

Totality: total
Visibility: public export

stringEq : x = y -> x == y = True

Totality: total
Visibility: public export

IsFieldStale : IsField nm flds -> fst nmv = nm -> (0 _ : nmv # flds) -> Void

Totality: total
Visibility: public export

IsFieldIrrelevant : (p : IsField nm flds) -> (q : IsField nm flds) -> p = q

Totality: total
Visibility: public export

isField : (fldName : String) -> (flds : Fields a) -> Dec (IsField fldName flds)

Totality: total
Visibility: public export

field : Any p flds -> Field a

Totality: total
Visibility: public export

.project : Record f flds -> (name : String) -> {auto pos : IsYes (isField name flds)} -> f (field (toWitness pos))

Totality: total
Visibility: public export

tabulate : (args : ArgList) -> ((arg : String) -> Any (\{arg:0} => arg = {arg:0}) args -> a arg) -> Fields a

Totality: total
Visibility: public export

0 tabulateFreshness : {0 a : String -> Type} -> (args : ArgList) -> (f : ((arg : String) -> Any (\{arg:0} => arg = {arg:0}) args -> a arg)) -> y # args -> (y ** u) # tabulate args f

Totality: total
Visibility: public export

map : ((nm : String) -> a nm -> b nm) -> Fields a -> Fields b

Totality: total
Visibility: public export

foldl : (b -> a -> b) -> b -> Record (const a) flds -> b

Totality: total
Visibility: public export

TypeFields : Record (const Type) flds -> Fields (const Type)

Totality: total
Visibility: public export

PartialRecord : (Field a -> Type) -> Fields a -> Type

Totality: total
Visibility: public export

traverse : Applicative m => ((x : Field a) -> f x -> m (g x)) -> Record f flds -> m (Record g flds)

Totality: total
Visibility: public export

sequence : Applicative g => Record (g . f) flds -> g (Record f flds)

Totality: total
Visibility: public export