Commit a924b931 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

keyword 'range' should be allowed as lident

parent aa0e76c9
......@@ -995,6 +995,7 @@ uident_nq:
lident:
| LIDENT { mk_id $1 $startpos $endpos }
| lident_keyword { mk_id $1 $startpos $endpos }
| LIDENT_QUOTE { mk_id $1 $startpos $endpos }
lident_nq:
......
......@@ -195,14 +195,14 @@ theory MapInjection
(** [surjective a n] is true when [a] is a surjection
from [(0..n-1)] to [(0..n-1)] *)
predicate range' (a: map int int) (n: int) =
predicate range (a: map int int) (n: int) =
forall i: int. 0 <= i < n -> 0 <= a[i] < n
(** [range' a n] is true when [a] maps the domain
(** [range a n] is true when [a] maps the domain
[(0..n-1)] into [(0..n-1)] *)
lemma injective_surjective:
forall a: map int int, n: int.
injective a n -> range' a n -> surjective a n
injective a n -> range a n -> surjective a n
(** main lemma: an injection on [(0..n-1)] that
ranges into [(0..n-1)] is also a surjection *)
......
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