Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit f4b952ef authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Mark Map.set as ghost, so that it can be used by examples/hashtbl_impl.

parent bb484dc9
......@@ -10,12 +10,12 @@ theory Map
let function get (f: map 'a 'b) (x: 'a) : 'b = f x
function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b =
let ghost function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b =
fun y -> if y = x then v else f y
(** syntactic sugar *)
let function ([]) (f: map 'a 'b) (x: 'a) : 'b = f x
function ([<-]) (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b = set f x v
let ghost function ([<-]) (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b = set f x v
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment