diff options
Diffstat (limited to 'test-suite/output/UnivBinders.out')
| -rw-r--r-- | test-suite/output/UnivBinders.out | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 128bc7767..904ff68aa 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -4,3 +4,9 @@ bar@{u} = nat *) bar is universe polymorphic +foo@{u Top.8 v} = +Type@{Top.8} -> Type@{v} -> Type@{u} + : Type@{max(u+1, Top.8+1, v+1)} +(* u Top.8 v |= *) + +foo is universe polymorphic |