 Jesper Cockx
|
994e2ca3fe
[ fix #3441 ] Fixed by changing an r to an l
|
6 лет назад |
 Nils Anders Danielsson
|
e68360b16a
[ refactor ] Removed some commented-out code.
|
6 лет назад |
|
Nils Anders Danielsson
|
e205a43e87
Fixed #1209.
|
6 лет назад |
 Ulf Norell
|
2a1ba9d744
[ fix #3461 ] proper constraint for stuck quoteTerm
|
6 лет назад |
|
Jesper Cockx
|
51c31307ea
[ fix #3460 ] Don't consider generalizable names to be in scope for interactive case splitting
|
6 лет назад |
|
Ulf Norell
|
9e936f0d67
Merge pull request #3455 from agda/issue3435
|
6 лет назад |
|
Ulf Norell
|
285415c49e
[ benchmarking ] add account for instance search
|
6 лет назад |
|
Ulf Norell
|
9153eccf51
[ #3435 ] refactor: get rid of special TC error only used locally by instance search
|
6 лет назад |
|
Ulf Norell
|
2c23d6bb8e
added come comments
|
6 лет назад |
|
Nils Anders Danielsson
|
63b7591cdf
Added a section "HTML backend" to the changelog for Agda 2.6.0.
|
6 лет назад |
|
Nils Anders Danielsson
|
b777e620c7
[ #3180 ] Removed more code.
|
6 лет назад |
 Andreas Abel
|
b444550a0e
[ Builtin.Nat ] documentation of Euclidean division [ci skip]
|
6 лет назад |
|
Jesper Cockx
|
7178ac325a
[ re #3000 ] Added test case
|
6 лет назад |
|
Jesper Cockx
|
1a3a3a74eb
[ re #3000 ] Add a missing reduce
|
6 лет назад |
|
Jesper Cockx
|
07fda331d8
[ doc ] Fix "hello world" example
|
6 лет назад |
|
Jesper Cockx
|
fa7ee0e679
[ fix #3434 ] Use canonical name of constructor for injectivity map
|
6 лет назад |
|
Andreas Abel
|
16b9796a64
fixed whitespace violation
|
6 лет назад |
|
Jesper Cockx
|
243d70f3cf
[ fix #3448 ] Use an empty map if there's no metadata for generalizable vars attached to a name
|
6 лет назад |
|
Jesper Cockx
|
8dcd2e2d14
[ re #2548 ] Add some misc information from the wiki
|
6 лет назад |
|
Jesper Cockx
|
105e0b5a07
[ re #2548 ] Add information on universe levels from the wiki
|
6 лет назад |
|
Jesper Cockx
|
aad6e92b71
[ re #2548 ] Add information on termination checking from the wiki
|
6 лет назад |
|
Ulf Norell
|
1b51287ad2
[ fix #3435 ] don't wake up instance constraints unnecessarily
|
6 лет назад |
 Andrea Vezzosi
|
14179aeb45
[ cubical #2446 ] Prevent modules from copying defs that have side conditions.
|
6 лет назад |
|
Ulf Norell
|
a31d2fd8dd
[ fix #2044 ] improve error messages for failed instance search
|
6 лет назад |
|
Ulf Norell
|
47358b3621
[ #3435 ] postpone instance constraints while checking applications
|
6 лет назад |
|
Jesper Cockx
|
0c58a6597a
[ fix #3443 ] Don't turn dot patterns into variables in missing clauses
|
6 лет назад |
|
Jesper Cockx
|
94b9736c43
[ re #3289 ] Postfix projections shouldn't have hiding information
|
6 лет назад |
|
Jesper Cockx
|
9936aeb053
[ fix #3452 ] If split fails because of irrelevance, try other splits instead of failing hard
|
6 лет назад |
|
Ulf Norell
|
3e4de0ace7
refactor: add export list to InstanceArguments
|
6 лет назад |
 G. Allais
|
41693c63c1
[ fix #2899 ] Ignore private definitions (#3450)
|
6 лет назад |
