diff options
| author | Gabriel Kerneis | 2013-11-11 10:25:37 +0000 |
|---|---|---|
| committer | Gabriel Kerneis | 2013-11-11 10:25:37 +0000 |
| commit | 4e005a7065f88fb2ba4888c51dc8c0508d867e3f (patch) | |
| tree | 97ff3f0af8ee6df1c7b18ad842e766e7678d8c17 /language/l2_parse.ott | |
| parent | b644c12a4b4e80120772b7379fbadf211825fc31 (diff) | |
| parent | 2c7bf65b9c256a0d9bc3e4a5dfdeb3c208da2d61 (diff) | |
Merge branch 'new-lem-lib'
Diffstat (limited to 'language/l2_parse.ott')
| -rw-r--r-- | language/l2_parse.ott | 23 |
1 files changed, 6 insertions, 17 deletions
diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 56152bd1..c2cbe50d 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -7,7 +7,7 @@ metavar num ::= {{ lex numeric }} {{ ocaml int }} {{ hol num }} - {{ lem num }} + {{ lem nat }} {{ com Numeric literals }} metavar hex ::= @@ -56,25 +56,14 @@ exception Parse_error_locn of l * string embed {{ lem -open Pmap -open Pervasives +open import Map +open import Maybe +open import Pervasives type l = | Unknown - | Trans of string * option l - | Range of num * num - -val disjoint : forall 'a . set 'a -> set 'a -> bool -let disjoint s1 s2 = - let diff = s1 inter s2 in - diff = Pervasives.empty - -val disjoint_all : forall 'a. list (set 'a) -> bool -let rec disjoint_all ls = match ls with - | [] -> true - | [a] -> true - | a::b::rs -> (disjoint a b) && (disjoint_all (b::rs)) -end + | Trans of string * maybe l + | Range of nat * nat val duplicates : forall 'a. list 'a -> list 'a |