package preface

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file lattice.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
module type LAWS = sig
  include Join_semilattice.LAWS
  include Meet_semilattice.LAWS with type t := t

  val lattice_1 : unit -> (t, t -> t) Law.t
  val lattice_2 : unit -> (t, t -> t) Law.t
end

module For (L : Preface_specs.LATTICE) : LAWS with type t := L.t = struct
  open Law
  include Join_semilattice.For (L)
  include Meet_semilattice.For (L)

  let lattice_1 () =
    let lhs a b = L.meet a (L.join a b)
    and rhs a _ = a in
    law ("meet a (join a b)" =~ lhs) ("a" =~ rhs)
  ;;

  let lattice_2 () =
    let lhs a b = L.join a (L.meet a b)
    and rhs a _ = a in
    law ("join a (meet a b)" =~ lhs) ("a" =~ rhs)
  ;;
end
OCaml

Innovation. Community. Security.