
  0 | module Control.Lens.Optic
  1 | 
  2 | import Data.Tensor
  3 | import Data.Profunctor
  4 | 
  5 | %default total
  6 | 
  7 | 
  8 | public export
  9 | Simple : (k -> k -> k' -> k' -> r) -> k -> k' -> r
 10 | Simple f s a = f s s a a
 11 | 
 12 | 
 13 | public export
 14 | Optic' : (p : Type -> Type -> Type) -> (s,t,a,b : Type) -> Type
 15 | Optic' p s t a b = p a b -> p s t
 16 | 
 17 | public export
 18 | 0 Optic : ((Type -> Type -> Type) -> Type) -> (s,t,a,b : Type) -> Type
 19 | Optic constr s t a b = forall p. constr p => Optic' p s t a b
 20 | 
 21 |