diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-09-08 10:23:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-09-08 17:09:43 +0200 |
| commit | 26a79004e47bbdc97df61015ce7e944eef14ac71 (patch) | |
| tree | 1f24c9acbb73cd63dcc689222b965f245767137e /test-suite/success/namedunivs.v | |
| parent | 89ad50f4d7e1312539995ced3a632821bf6af7c5 (diff) | |
Parsing of Type@{max(i,j)}.
Diffstat (limited to 'test-suite/success/namedunivs.v')
| -rw-r--r-- | test-suite/success/namedunivs.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v index 5c0a3c7f2..059462fac 100644 --- a/test-suite/success/namedunivs.v +++ b/test-suite/success/namedunivs.v @@ -30,6 +30,9 @@ Definition foo' {A : Type@{i}} (o : option@{i} A) : option@{i} A := Definition foo'' {A : Type@{i}} (o : option@{j} A) : option@{k} A := o. + +Definition testm (A : Type@{i}) : Type@{max(i,j)} := A. + (* Inductive prod (A : Type@{i}) (B : Type@{j}) := *) (* | pair : A -> B -> prod A B. *) @@ -43,7 +46,6 @@ Definition foo'' {A : Type@{i}} (o : option@{j} A) : option@{k} A := (* | pair _ _ a b => b *) (* end. *) - (* Inductive paths {A : Type} : A -> A -> Type := *) (* | idpath (a : A) : paths a a. *) |