For (preface.Preface_laws.Indexed

Parameters

module A : Preface_specs.INDEXED_APPLICATIVE

include Indexed_apply.LAWS with type ('a, 'index) t := ('a, 'index) A.t

include Indexed_functor.LAWS with type ('a, 'index) t := ('a, 'index) A.t

val functor_1 : unit -> (('a, 'index) A.t, ('a, 'index) A.t) Law.t

val functor_2 : 
  unit ->
  ('a -> 'b, ('c -> 'a) -> ('c, 'index) A.t -> ('b, 'index) A.t) Law.t

val apply_1 : 
  unit ->
  ((unit, 'index) A.t, ('a, 'index) A.t -> ('a, 'index) A.t) Law.t

val apply_2 : 
  unit ->
  (('a, 'index) A.t, (unit, 'index) A.t -> ('a, 'index) A.t) Law.t

val applicative_1 : unit -> (('a, 'index) A.t, ('a, 'index) A.t) Law.t

val applicative_2 : unit -> ('a -> 'b, 'a -> ('b, 'index) A.t) Law.t

val applicative_3 : 
  unit ->
  (('a -> 'b, 'index) A.t, 'a -> ('b, 'index) A.t) Law.t

val applicative_4 : 
  unit ->
  (('a -> 'b, 'index) A.t,
    ('c -> 'a, 'index) A.t ->
    ('c, 'index) A.t ->
    ('b, 'index) A.t)
    Law.t

val applicative_5 : 
  unit ->
  ('a -> 'b, ('a, 'index) A.t -> ('b, 'index) A.t) Law.t