diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-20 19:45:43 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 14:18:35 +0100 |
commit | 280c922fc55b57c430cad721c83650a796a375fd (patch) | |
tree | 5f0c9c20a75532ba134bbde6f428facefceb5125 /test-suite/output | |
parent | c93d5094bff73498ec8fc02837e16cc5ce9103b6 (diff) |
Allow local universe renaming in Print.
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/UnivBinders.out | 31 | ||||
-rw-r--r-- | test-suite/output/UnivBinders.v | 19 |
2 files changed, 50 insertions, 0 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 42fb52a3b..6fb8cba18 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -53,3 +53,34 @@ Monomorphic mono = Type@{u} (* {u} |= *) mono is not universe polymorphic +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. diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 2c378e795..46904b384 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -33,3 +33,22 @@ Print foo. (* Binders even work with monomorphic definitions! *) Monomorphic Definition mono@{u} := Type@{u}. Print mono. + +(* Using local binders for printing. *) +Print foo@{E M N}. +(* Underscores discard the name if there's one. *) +Print foo@{_ _ _}. + +(* Also works for inductives and records. *) +Print Empty@{E}. +Print PWrap@{E}. + +(* Also works for About. *) +About punwrap@{K}. + +(* Instance length check. *) +Fail Print foo@{E}. +Fail Print mono@{E}. + +(* Not everything can be printed with custom universe names. *) +Fail Print Coq.Init.Logic@{E}. |