issues
search
agda
/
agda
Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.4k
stars
339
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Expose constructor erasure in reflection interface
#7322
cmcmA20
opened
2 days ago
0
No warning about useless `{-# CATCHALL #-}` pragma
#7321
andreasabel
opened
4 days ago
0
Turn on --exact-split by default
#7320
andreasabel
closed
3 days ago
0
Make --postfix-projections the default
#7319
andreasabel
closed
3 days ago
0
`--postfix-projections` do not make use of mixfix syntax
#7318
andreasabel
closed
3 days ago
1
Don't mark eta unit records as irrelevant
#7317
UlfNorell
closed
5 days ago
0
add \crossmark to emacs input mode
#7316
UlfNorell
closed
4 days ago
0
same shadowing logic for record patterns as for constructor patterns in absToCon
#7315
UlfNorell
closed
5 days ago
0
Add constructors for custom backend warning/errors
#7314
UlfNorell
closed
6 days ago
0
Update universe-levels.lagda.rst
#7313
hawkinsw
closed
1 week ago
2
Normalization gives trivial `transp`
#7312
Trebor-Huang
closed
1 week ago
1
[ #6406 ] Add test cases from discussion on this issue
#7311
jespercockx
closed
6 days ago
1
Add `workOnTypes` reflection primitive
#7310
jespercockx
closed
6 days ago
0
fix #6141: don't generalize over metas constrained by instance search
#7309
UlfNorell
opened
1 week ago
1
Turn on -fdebug in default make targets
#7308
UlfNorell
closed
1 week ago
0
fix #7017: document instance projections
#7307
UlfNorell
closed
1 week ago
0
Fix #7304: ignore abstract mode when building the instance discrimination tree
#7306
UlfNorell
closed
1 week ago
3
Fix #7286: don't fail hard when there are instances with unresolved types
#7305
UlfNorell
closed
1 week ago
0
Bad interaction between instance search and opaque
#7304
UlfNorell
closed
1 week ago
6
Revert cyclic computation of ranges (and ban `mdo` from this code base)
#7303
andreasabel
opened
2 weeks ago
2
Fix #7301 (loop in parser): move verifyRecordDirectives to scope checker
#7302
andreasabel
closed
2 weeks ago
0
Agda >=2.6.3 hangs on conflicting record directives
#7301
andreasabel
closed
2 weeks ago
4
New deadcode warning CoinductiveEtaRecord instead of GenericError
#7300
andreasabel
closed
3 days ago
0
Testsuite: heads up: with GHC 9.10, `throw` will print a callstack
#7299
andreasabel
opened
2 weeks ago
0
Remove fiddly attempt at instance postponement
#7298
plt-amy
closed
2 weeks ago
4
GenericDocErrors to new errors LibraryError and RecursiveRecordNeedsInductivity
#7297
andreasabel
closed
2 weeks ago
0
U+02B3 (MODIFIER SMALL LETTER R, aka superscript r) not available via \^r
#7296
nrnrnr
closed
2 weeks ago
4
with-abstraction regression
#7295
UlfNorell
closed
2 weeks ago
6
fail in solving instance of `⊆-refl` in Agda 2.6.4.3
#7294
mechvel
closed
2 weeks ago
12
Failed to write interface /usr/share/Agda-stdlib/_build/2.6.4.3/agda/src/Data/Unit/Base.agdai.
#7293
juhp
opened
3 weeks ago
2
New error warning `ConstructorDoesNotFitInData` instead of hard error.
#7292
andreasabel
closed
3 weeks ago
0
Recursion with records
#7291
txa
opened
3 weeks ago
1
Latex backend/package bug: `! Package array Error: Empty preamble: 'l' used.`
#7290
WhatisRT
opened
3 weeks ago
4
`--lossy-unification` doesn't fall back to regular unification when instances are used
#7289
Thrithralas
opened
3 weeks ago
2
Compatibiilty of partial elements defined using cubical face lattice generators with reflextion machinery
#7288
marcinjangrzybowski
opened
3 weeks ago
0
Temporary fix for reflection of partial elements.
#7287
marcinjangrzybowski
opened
3 weeks ago
0
Hard error on `instance` definition with unsolved type
#7286
UlfNorell
closed
1 week ago
0
TBT: no termination error with `--double-check`
#7285
andreasabel
opened
1 month ago
0
TBT does not termination-check record type definitions
#7284
andreasabel
opened
1 month ago
0
agdaLatex documentation
#7283
csetzer
closed
1 month ago
0
bump ci ghc 9.10.1
#7282
andreasabel
closed
1 month ago
0
[refactor] __FROM_JUST__ = fromMaybe __IMPOSSIBLE__
#7281
omelkonian
opened
1 month ago
2
Fix CI breakage caused by new (2024-05-14) runner images
#7280
andreasabel
closed
1 month ago
0
TBT: internal error in function `smallerOrEq`
#7279
andreasabel
opened
1 month ago
1
TBT: no function nor calls listed in termination error
#7278
andreasabel
opened
1 month ago
0
TBT: do not count rhs `j : Size< i` towards `j < i` in termination
#7277
andreasabel
opened
1 month ago
0
#7191: respect abstract mode when using show function
#7276
UlfNorell
closed
1 month ago
0
#7245: warn about INJECTIVE_FOR_INFERENCE on non-functions
#7275
UlfNorell
closed
1 month ago
0
#7182: copied records should refer to the copied constructor and fields
#7274
UlfNorell
closed
1 month ago
0
ToTreeless: allow backends to define custom pipelines
#7273
omelkonian
closed
1 month ago
0
Next