From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/output/UnivBinders.out | 181 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 181 insertions(+) create mode 100644 test-suite/output/UnivBinders.out (limited to 'test-suite/output/UnivBinders.out') diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out new file mode 100644 index 00000000..23379afd --- /dev/null +++ b/test-suite/output/UnivBinders.out @@ -0,0 +1,181 @@ +NonCumulative Inductive Empty@{u} : Type@{u} := +NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } + +PWrap has primitive projections with eta conversion. +For PWrap: Argument scope is [type_scope] +For pwrap: Argument scopes are [type_scope _] +punwrap@{u} = +fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p + : forall A : Type@{u}, PWrap@{u} A -> A +(* u |= *) + +punwrap is universe polymorphic +Argument scopes are [type_scope _] +NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } + +For RWrap: Argument scope is [type_scope] +For rwrap: Argument scopes are [type_scope _] +runwrap@{u} = +fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap + : forall A : Type@{u}, RWrap@{u} A -> A +(* u |= *) + +runwrap is universe polymorphic +Argument scopes are [type_scope _] +Wrap@{u} = fun A : Type@{u} => A + : Type@{u} -> Type@{u} +(* u |= *) + +Wrap is universe polymorphic +Argument scope is [type_scope] +wrap@{u} = +fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap + : forall A : Type@{u}, Wrap@{u} A -> A +(* u |= *) + +wrap is universe polymorphic +Arguments A, Wrap are implicit and maximally inserted +Argument scopes are [type_scope _] +bar@{u} = nat + : Wrap@{u} Set +(* u |= Set < u + *) + +bar is universe polymorphic +foo@{u Top.17 v} = +Type@{Top.17} -> Type@{v} -> Type@{u} + : Type@{max(u+1,Top.17+1,v+1)} +(* u Top.17 v |= *) + +foo is universe polymorphic +Type@{i} -> Type@{j} + : Type@{max(i+1,j+1)} +(* {j i} |= *) + = Type@{i} -> Type@{j} + : Type@{max(i+1,j+1)} +(* {j i} |= *) +Monomorphic mono = Type@{mono.u} + : Type@{mono.u+1} +(* {mono.u} |= *) + +mono is not universe polymorphic +mono + : Type@{mono.u+1} +Type@{mono.u} + : Type@{mono.u+1} +The command has indeed failed with message: +Universe u already exists. +monomono + : Type@{MONOU+1} +mono.monomono + : Type@{mono.MONOU+1} +monomono + : Type@{MONOU+1} +mono + : Type@{mono.u+1} +The command has indeed failed with message: +Universe u already exists. +bobmorane = +let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff + : Type@{max(tt.u,ff.u)} +The command has indeed failed with message: +Universe u already bound. +foo@{E M N} = +Type@{M} -> Type@{N} -> Type@{E} + : Type@{max(E+1,M+1,N+1)} +(* E M N |= *) + +foo is universe polymorphic +foo@{Top.16 Top.17 Top.18} = +Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16} + : Type@{max(Top.16+1,Top.17+1,Top.18+1)} +(* Top.16 Top.17 Top.18 |= *) + +foo is universe polymorphic +NonCumulative Inductive Empty@{E} : Type@{E} := +NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } + +PWrap has primitive projections with eta conversion. +For PWrap: Argument scope is [type_scope] +For pwrap: Argument scopes are [type_scope _] +punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A +(* K |= *) + +punwrap is universe polymorphic +Argument scopes are [type_scope _] +punwrap is transparent +Expands to: Constant Top.punwrap +The command has indeed failed with message: +Universe instance should have length 3 +The command has indeed failed with message: +Universe instance should have length 0 +The command has indeed failed with message: +This object does not support universe names. +The command has indeed failed with message: +Cannot enforce v < u because u < gU < gV < v +Monomorphic bind_univs.mono = +Type@{bind_univs.mono.u} + : Type@{bind_univs.mono.u+1} +(* {bind_univs.mono.u} |= *) + +bind_univs.mono is not universe polymorphic +bind_univs.poly@{u} = Type@{u} + : Type@{u+1} +(* u |= *) + +bind_univs.poly is universe polymorphic +insec@{v} = Type@{u} -> Type@{v} + : Type@{max(u+1,v+1)} +(* v |= *) + +insec is universe polymorphic +insec@{u v} = Type@{u} -> Type@{v} + : Type@{max(u+1,v+1)} +(* u v |= *) + +insec is universe polymorphic +inmod@{u} = Type@{u} + : Type@{u+1} +(* u |= *) + +inmod is universe polymorphic +SomeMod.inmod@{u} = Type@{u} + : Type@{u+1} +(* u |= *) + +SomeMod.inmod is universe polymorphic +inmod@{u} = Type@{u} + : Type@{u+1} +(* u |= *) + +inmod is universe polymorphic +Applied.infunct@{u v} = +inmod@{u} -> Type@{v} + : Type@{max(u+1,v+1)} +(* u v |= *) + +Applied.infunct is universe polymorphic +axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i} +(* i Top.48 Top.49 |= *) + +axfoo is universe polymorphic +Argument scope is [type_scope] +Expands to: Constant Top.axfoo +axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i} +(* i Top.48 Top.49 |= *) + +axbar is universe polymorphic +Argument scope is [type_scope] +Expands to: Constant Top.axbar +axfoo' : Type@{Top.51} -> Type@{axbar'.i} + +axfoo' is not universe polymorphic +Argument scope is [type_scope] +Expands to: Constant Top.axfoo' +axbar' : Type@{Top.51} -> Type@{axbar'.i} + +axbar' is not universe polymorphic +Argument scope is [type_scope] +Expands to: Constant Top.axbar' +The command has indeed failed with message: +When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block). -- cgit v1.2.3