diff options
| author | Pierre-Marie Pédrot | 2019-10-14 07:05:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-14 07:05:01 +0200 |
| commit | 54e31c28bf21caf7f8fcff1fcf4b415fed66dc3a (patch) | |
| tree | 038374a730db66e8a2284f7b186925a654a7369e /test-suite | |
| parent | 7623da4448381955ef063dcce6f4263d91fe0d74 (diff) | |
| parent | 825d0737069debb8e16c44cd49ad3a273211f76c (diff) | |
Merge PR #10811: Allow SProp default on
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/UnivBinders.out | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index d13ea707bb..d48d8b900f 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -38,10 +38,10 @@ Argument scopes are [type_scope _] bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) -foo@{u UnivBinders.17 v} = -Type@{UnivBinders.17} -> Type@{v} -> Type@{u} - : Type@{max(u+1,UnivBinders.17+1,v+1)} -(* u UnivBinders.17 v |= *) +foo@{u UnivBinders.18 v} = +Type@{UnivBinders.18} -> Type@{v} -> Type@{u} + : Type@{max(u+1,UnivBinders.18+1,v+1)} +(* u UnivBinders.18 v |= *) Type@{i} -> Type@{j} : Type@{max(i+1,j+1)} (* {j i} |= *) @@ -68,19 +68,19 @@ mono The command has indeed failed with message: Universe u already exists. bobmorane = -let tt := Type@{UnivBinders.33} in -let ff := Type@{UnivBinders.35} in tt -> ff - : Type@{max(UnivBinders.32,UnivBinders.34)} +let tt := Type@{UnivBinders.34} in +let ff := Type@{UnivBinders.36} in tt -> ff + : Type@{max(UnivBinders.33,UnivBinders.35)} 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@{u UnivBinders.17 v} = -Type@{UnivBinders.17} -> Type@{v} -> Type@{u} - : Type@{max(u+1,UnivBinders.17+1,v+1)} -(* u UnivBinders.17 v |= *) +foo@{u UnivBinders.18 v} = +Type@{UnivBinders.18} -> Type@{v} -> Type@{u} + : Type@{max(u+1,UnivBinders.18+1,v+1)} +(* u UnivBinders.18 v |= *) Inductive Empty@{E} : Type@{E} := (* E |= *) Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } @@ -143,16 +143,16 @@ Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) -axfoo@{i UnivBinders.57 UnivBinders.58} : -Type@{UnivBinders.57} -> Type@{i} -(* i UnivBinders.57 UnivBinders.58 |= *) +axfoo@{i UnivBinders.59 UnivBinders.60} : +Type@{UnivBinders.59} -> Type@{i} +(* i UnivBinders.59 UnivBinders.60 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo -axbar@{i UnivBinders.57 UnivBinders.58} : -Type@{UnivBinders.58} -> Type@{i} -(* i UnivBinders.57 UnivBinders.58 |= *) +axbar@{i UnivBinders.59 UnivBinders.60} : +Type@{UnivBinders.60} -> Type@{i} +(* i UnivBinders.59 UnivBinders.60 |= *) axbar is universe polymorphic Argument scope is [type_scope] |