
  0 | module Control.RecordB
  1 | 
  2 | import Monocle.Lens
  3 | 
  4 | %default total
  5 | 
  6 | public export
  7 | interface RecordB (0 k : Type) (0 t : (k -> Type) -> Type) | t where
  8 |   constructor MkRecordB
  9 |   field : (0 f : k -> Type) -> (v : k) -> Lens' (t f) (f v)
 10 | 
 11 | export %inline
 12 | field' : RecordB k t => (v : k) -> Lens' (t f) (f v)
 13 | field' = field f
 14 | 
 15 | export %inline
 16 | getField : RecordB k t => (v : k) -> t f -> f v
 17 | getField v = get_ (field f v)
 18 | 
 19 | export %inline
 20 | setField : RecordB k t => (v : k) -> f v -> t f -> t f
 21 | setField v = setL (field f v)
 22 |