Data.Record.SmartConstructors

Selectively ported from agdARGS's Data.Recrod.SmartConstructors

Please port more if you want!

Definitions

record Checkable : (Field a -> Type) -> Fields a -> Type

Totality: total
Visibility: public export
Constructor: 

MkCheckable : Record f flds -> Checkable f flds

Projection: 

.mkCheckable : Checkable f flds -> Record f flds

.mkCheckable : Checkable f flds -> Record f flds

Totality: total
Visibility: public export

mkCheckable : Checkable f flds -> Record f flds

Totality: total
Visibility: public export

record Entry : (a : (String -> Type)) -> (Field a -> Type) -> Fields a -> Type

Totality: total
Visibility: public export
Constructor: 

(::=) : (name : String) -> {auto 0 pos : IsYes (isField name flds)} -> f (field (toWitness pos)) -> Entry a f flds

Projections:

.name : Entry a f flds -> String

0 .pos : ({rec:0} : Entry a f flds) -> IsYes (isField (name {rec:0}) flds)

.value : ({rec:0} : Entry a f flds) -> f (field (toWitness (pos {rec:0})))

.name : Entry a f flds -> String

Totality: total
Visibility: public export

name : Entry a f flds -> String

Totality: total
Visibility: public export

0 .pos : ({rec:0} : Entry a f flds) -> IsYes (isField (name {rec:0}) flds)

Totality: total
Visibility: public export

0 pos : ({rec:0} : Entry a f flds) -> IsYes (isField (name {rec:0}) flds)

Totality: total
Visibility: public export

.value : ({rec:0} : Entry a f flds) -> f (field (toWitness (pos {rec:0})))

Totality: total
Visibility: public export

value : ({rec:0} : Entry a f flds) -> f (field (toWitness (pos {rec:0})))

Totality: total
Visibility: public export

Nil : Checkable f []

Totality: total
Visibility: public export

(::) : (entry : Entry a f flds) -> Checkable f (remove (toWitness (entry .pos))) -> Checkable f flds

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

record Inferrable : (Field a -> Type) -> Fields a -> Type

Totality: total
Visibility: public export
Constructor: 

MkInferrable : Record f flds -> Inferrable f flds

Projection: 

.mkInferrable : Inferrable f flds -> Record f flds

.mkInferrable : Inferrable f flds -> Record f flds

Totality: total
Visibility: public export

mkInferrable : Inferrable f flds -> Record f flds

Totality: total
Visibility: public export

record Entry : (a : (String -> Type)) -> (Field a -> Type) -> Type

Totality: total
Visibility: public export
Constructor: 

(::=) : (name : String) -> f (name ** type) -> Entry a f

Projections:

.name : Entry a f -> String

.type : ({rec:0} : Entry a f) -> a (name {rec:0})

.value : ({rec:0} : Entry a f) -> f (name {rec:0} ** type {rec:0})

.name : Entry a f -> String

Totality: total
Visibility: public export

name : Entry a f -> String

Totality: total
Visibility: public export

.type : ({rec:0} : Entry a f) -> a (name {rec:0})

Totality: total
Visibility: public export

type : ({rec:0} : Entry a f) -> a (name {rec:0})

Totality: total
Visibility: public export

.value : ({rec:0} : Entry a f) -> f (name {rec:0} ** type {rec:0})

Totality: total
Visibility: public export

value : ({rec:0} : Entry a f) -> f (name {rec:0} ** type {rec:0})

Totality: total
Visibility: public export

Nil : Inferrable f []

Totality: total
Visibility: public export

(::) : (entry : Entry a f) -> Inferrable f flds -> {auto 0 fresh : (entry .name ** entry .type) # flds} -> Inferrable f ((entry .name ** entry .type) :: flds)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

BasicRecord : (Type -> Type) -> Fields (const Type) -> Type

  A record where the notion of type for its fields is `Type` itself

Totality: total
Visibility: public export

mkBasicRecord : BasicRecord f flds -> BasicRecord f flds

  This acts as a type annotation ensuring the list passed as an
  argument is a basic record.

Totality: total
Visibility: public export