 caryoscelus
|
4a213434e2
[ doc ] reflection: add declaration unquote example
|
%!s(int64=6) %!d(string=hai) anos |
|
caryoscelus
|
2c077f2c1e
[ refactor ] remove Ranged wrapper from Inductive in records
|
%!s(int64=6) %!d(string=hai) anos |
|
caryoscelus
|
a2a115a6b0
[ git ] ignore .emacs* files
|
%!s(int64=6) %!d(string=hai) anos |
|
caryoscelus
|
92373bde18
[ cleanup ] remove unused function
|
%!s(int64=6) %!d(string=hai) anos |
|
caryoscelus
|
73cc22d519
[ test suite ] remove orphaned .err files from test/Fail
|
%!s(int64=6) %!d(string=hai) anos |
 G. Allais
|
98d6f195fe
[ fix ] using Common.IO rather than postulates (#3472)
|
%!s(int64=6) %!d(string=hai) anos |
|
Guillaume Allais
|
350c3e20c4
[ fix ] adding COMPILE JS pragma
|
%!s(int64=6) %!d(string=hai) anos |
|
Guillaume Allais
|
b5beca5e90
[ fix ] using experimental branch of agda-stdlib
|
%!s(int64=6) %!d(string=hai) anos |
 Andrés Sicard-Ramírez
|
0366a7956c
[ fixed #3444 ] Fixed `Setup.hs` when using Cabal >= 2.0.0.0.
|
%!s(int64=6) %!d(string=hai) anos |
|
Andrés Sicard-Ramírez
|
d606f41bb4
[ Setup.hs ] Only cosmetics.
|
%!s(int64=6) %!d(string=hai) anos |
 Jesper Cockx
|
fea04acf6b
[ re #3463 ] fix test case
|
%!s(int64=6) %!d(string=hai) anos |
|
Jesper Cockx
|
eae4d60f2d
[ fix #3463 ] Use name "r" for argument of instance-opened record
|
%!s(int64=6) %!d(string=hai) anos |
|
Jesper Cockx
|
93c4b76b0c
[ re #3463 ] Add some debug output
|
%!s(int64=6) %!d(string=hai) anos |
|
Jesper Cockx
|
def0b01cf9
[ #3464 ] Added test case
|
%!s(int64=6) %!d(string=hai) anos |
|
Jesper Cockx
|
cd6cee087e
[ fix #3358 ] Postpone instance search until after generalization
|
%!s(int64=6) %!d(string=hai) anos |
|
Jesper Cockx
|
ca4fceabfc
[ re #3358 ] Wait with instance search if we cannot determine whether the type of a context variable is a record type
|
%!s(int64=6) %!d(string=hai) anos |
|
Jesper Cockx
|
bf84bbb87f
[ refactor ] Generalize some type signatures
|
%!s(int64=6) %!d(string=hai) anos |
 Andrea Vezzosi
|
5009287058
[ cubical ] Use the standard def. of fiber in Glue prims.
|
%!s(int64=6) %!d(string=hai) anos |
|
Andrea Vezzosi
|
fdb43152aa
[ Fixed #2788 ] Cubical builtins/prims require --cubical
|
%!s(int64=6) %!d(string=hai) anos |
|
Guillaume Allais
|
24bd9144a5
[ fix ] test case
|
%!s(int64=6) %!d(string=hai) anos |
|
Andrea Vezzosi
|
e3d77891ce
[ #2446 ] Test cases.
|
%!s(int64=6) %!d(string=hai) anos |
|
Andrea Vezzosi
|
a78443792c
Merge branch 'issue3318'
|
%!s(int64=6) %!d(string=hai) anos |
 Ulf Norell
|
ee4a2b1ef8
[ fix #3354 ] order generalized variables by mention instead of definition site
|
%!s(int64=6) %!d(string=hai) anos |
|
Andrea Vezzosi
|
6e1b11e663
[ cubical #3318 ] Removed unused primitives and bound the others
|
%!s(int64=6) %!d(string=hai) anos |
|
Ulf Norell
|
daf656af19
[ fix #3401 ] give a telescope of the right length to the gentel-record pre-definition
|
%!s(int64=6) %!d(string=hai) anos |
|
Ulf Norell
|
e3089b2ee6
[ #3401 ] improve some debug output
|
%!s(int64=6) %!d(string=hai) anos |
|
Ulf Norell
|
b9320245d5
[ #3441 ] added missing golden value
|
%!s(int64=6) %!d(string=hai) anos |
|
Ulf Norell
|
4efe14bbe3
[ fix #3410 ] iterate forcing translation as long as it's making progress
|
%!s(int64=6) %!d(string=hai) anos |
|
Ulf Norell
|
cb452cf4ae
[ fix #3362 ] do 'constructs'-check before generalization
|
%!s(int64=6) %!d(string=hai) anos |
|
Ulf Norell
|
43551db2ed
[ #3362 ] refactor: allow generalizeType returning addtional information
|
%!s(int64=6) %!d(string=hai) anos |
