Why3 Standard Library index


Option type

module Option

  type option 'a = None | Some 'a

  let predicate is_none (o: option 'a)
    ensures { result <-> o = None }
  =
    match o with None -> true | Some _ -> false end

end

Generated by why3doc 1.0.0