diff options
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 |