aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Wellfounded/Lexicographic_Exponentiation.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Wellfounded/Lexicographic_Exponentiation.v')
-rw-r--r--theories/Wellfounded/Lexicographic_Exponentiation.v13
1 files changed, 7 insertions, 6 deletions
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 5bf2cedaa..06a9c123d 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -30,17 +30,18 @@ Syntactic Definition Cons := (cons 1!A).
Syntax constr
level 1:
- List [<<(list A)>>] -> ["List"]
- | Nil [<<(nil A)>>] -> ["Nil"]
- | Cons [<<(cons A)>>] -> ["Cons"]
+ List [ (list A) ] -> ["List"]
+ | Nil [ (nil A) ] -> ["Nil"]
+ | Cons [ (cons A) ] -> ["Cons"]
;
level 10:
- Cons2 [<<(cons A $e $l)>>] -> ["Cons " $e:L " " $l:L ].
+ Cons2 [ (cons A $e $l) ] -> ["Cons " $e:L " " $l:L ].
Hints Resolve d_one d_nil t_step.
-Syntax constr level 1:
- pair_sig [<<(exist (list A) Desc $e $d)>>] -> ["<<" $e:L "," $d:L ">>"].
+Syntax constr
+ level 1:
+ pair_sig [ (exist (list A) Desc $e $d) ] -> ["<<" $e:L "," $d:L ">>"].
Lemma left_prefix : (x,y,z:List)(ltl x^y z)-> (ltl x z).