diff options
| author | Pierre-Marie Pédrot | 2019-02-18 13:09:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-18 13:09:14 +0100 |
| commit | a59574c8eb4bdda60e4bdd6197e8a32574985588 (patch) | |
| tree | e15e1a0f78d23cd263726d725c93a5e6ce453465 /test-suite/output | |
| parent | f8d6c322783577b31cf55f8b55568ac56104202b (diff) | |
| parent | a9f0fd89cf3bb4b728eb451572a96f8599211380 (diff) | |
Merge PR #9439: Separate variance and universe fields in inductives.
Ack-by: ppedrot
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/UnivBinders.out | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index a960fe3441..222a808768 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,5 +1,7 @@ Inductive Empty@{u} : Type@{u} := +(* u |= *) Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } +(* u |= *) PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] @@ -11,6 +13,7 @@ fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p Argument scopes are [type_scope _] Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } +(* u |= *) For RWrap: Argument scope is [type_scope] For rwrap: Argument scopes are [type_scope _] @@ -79,7 +82,9 @@ Type@{UnivBinders.17} -> Type@{v} -> Type@{u} : Type@{max(u+1,UnivBinders.17+1,v+1)} (* u UnivBinders.17 v |= *) Inductive Empty@{E} : Type@{E} := +(* E |= *) Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } +(* E |= *) PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] @@ -109,7 +114,9 @@ bind_univs.poly@{u} = Type@{u} insec@{v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* v |= *) -Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} +Inductive insecind@{k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{k} +(* k |= *) For inseccstr: Argument scope is [type_scope] insec@{u v} = Type@{u} -> Type@{v} @@ -117,6 +124,7 @@ insec@{u v} = Type@{u} -> Type@{v} (* u v |= *) Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} +(* u k |= *) For inseccstr: Argument scope is [type_scope] insec2@{u} = Prop |