diff options
| author | Gaëtan Gilbert | 2020-02-13 16:52:33 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-19 14:09:01 +0100 |
| commit | 2ed097cfba9136a0fba9b961d24c408077fac11d (patch) | |
| tree | 6d3926e3d8aa20fd21929ad538f626660874b239 /test-suite | |
| parent | 43c3c7d6f62a9bee4772242c27fbafd54770d271 (diff) | |
ComInductive: use lbound=Prop iff non polymorphic
This avoids having to interp params and intern arities twice.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/UnivBinders.out | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 525ca48bee..04514c15cb 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -67,9 +67,9 @@ mono The command has indeed failed with message: Universe u already exists. bobmorane = -let tt := Type@{UnivBinders.34} in -let ff := Type@{UnivBinders.36} in tt -> ff - : Type@{max(UnivBinders.33,UnivBinders.35)} +let tt := Type@{UnivBinders.33} in +let ff := Type@{UnivBinders.35} in tt -> ff + : Type@{max(UnivBinders.32,UnivBinders.34)} The command has indeed failed with message: Universe u already bound. foo@{E M N} = @@ -142,16 +142,16 @@ Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) -axfoo@{i UnivBinders.59 UnivBinders.60} : -Type@{UnivBinders.59} -> Type@{i} -(* i UnivBinders.59 UnivBinders.60 |= *) +axfoo@{i UnivBinders.58 UnivBinders.59} : +Type@{UnivBinders.58} -> Type@{i} +(* i UnivBinders.58 UnivBinders.59 |= *) axfoo is universe polymorphic Arguments axfoo _%type_scope Expands to: Constant UnivBinders.axfoo -axbar@{i UnivBinders.59 UnivBinders.60} : -Type@{UnivBinders.60} -> Type@{i} -(* i UnivBinders.59 UnivBinders.60 |= *) +axbar@{i UnivBinders.58 UnivBinders.59} : +Type@{UnivBinders.59} -> Type@{i} +(* i UnivBinders.58 UnivBinders.59 |= *) axbar is universe polymorphic Arguments axbar _%type_scope |