appmap.mlw 412 Bytes
Newer Older
1 2 3 4 5

(** {2 Applicative maps} *)

module Appmap

6 7
  use map.Map
  use map.Const
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22

  type key

  type t 'a = abstract { contents: map key 'a }

  val function create (x: 'a): t 'a
    ensures { result.contents = const x }

  val function ([]) (m: t 'a) (k: key): 'a
    ensures { result = m.contents[k] }

  val function ([<-]) (m: t 'a) (k: key) (v: 'a): t 'a
    ensures { result.contents = m.contents[k <- v] }

end