Control.RecordB

Definitions

interface RecordB : (k : Type) -> ((k -> Type) -> Type) -> Type

Parameters: k, t
Constructor: 

MkRecordB

Methods:

field : (0 f : (k -> Type)) -> (v : k) -> Lens' (t f) (f v)

field : RecordB k t => (0 f : (k -> Type)) -> (v : k) -> Lens' (t f) (f v)

Totality: total
Visibility: public export

field' : RecordB k t => (v : k) -> Lens' (t f) (f v)

Totality: total
Visibility: export

getField : RecordB k t => (v : k) -> t f -> f v

Totality: total
Visibility: export

setField : RecordB k t => (v : k) -> f v -> t f -> t f

Totality: total
Visibility: export