[Why3-club] typo in doc

Jean-Jacques Levy jean-jacques.levy at inria.fr
Tue Mar 18 05:16:06 CET 2014


Dear Friends, 

the comment in theory/map is not correct:
------------
lemma occ_bounds: forall v: 'a, m: map int 'a, l u: int. 
    l <= u -> 0 <= occ v m l u <= u - l
(* direct when l>=u, by induction on b when l <= u *)
------------
-JJ-




More information about the Why3-club mailing list