 Jesper Cockx
|
fa09a8fe74
[ re #4908 ] add explicit --sized-types flag to test suite
|
%!s(int64=3) %!d(string=hai) anos |
 Andreas Abel
|
a8077a5997
[ #5000 ] Bring back SizeUniv
|
%!s(int64=4) %!d(string=hai) anos |
 Fredrik Nordvall Forsberg
|
a50ff581f3
[ #2487 ] consistency checking of options
|
%!s(int64=6) %!d(string=hai) anos |
 Nils Anders Danielsson
|
941676bc19
Fixed #2931: Renamed Agda.Builtin.Size.ω to ∞.
|
%!s(int64=7) %!d(string=hai) anos |
 Ulf Norell
|
a751e811a8
[ test ] use Agda.Builtin.* in test/Common
|
%!s(int64=9) %!d(string=hai) anos |
|
Andreas Abel
|
531b71d650
[ Issue 1428 ] Size BUILTINs no longer need postulates.
|
%!s(int64=10) %!d(string=hai) anos |
|
Andreas Abel
|
5c02b29c14
Added Size< to test/Common/Size.agda.
|
%!s(int64=11) %!d(string=hai) anos |
|
Andreas Abel
|
76f474bab3
Fixed polarity computation. Must be done after positivity check.
|
%!s(int64=13) %!d(string=hai) anos |
