Why3 Standard Library index


Applicative maps

module Appmap

  use map.Map
  use map.Const

  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

Generated by why3doc 1.2.0