diff options
| author | Gaëtan Gilbert | 2019-01-30 14:39:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-17 15:44:30 +0100 |
| commit | a9f0fd89cf3bb4b728eb451572a96f8599211380 (patch) | |
| tree | 577b7330af67793041cfaba8414005f93fc49c88 /test-suite/output | |
| parent | a49077ef67b8e70696ecacc311fc3070d1b7b461 (diff) | |
Separate variance and universe fields in inductives.
I think the usage looks cleaner this way.
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 |