Issues
- 0
wrong type for unnamed record constructor
#7329 opened by UlfNorell - 0
Internal error on pattern lambda with no clauses
#7326 opened by UlfNorell - 0
HTML backend: inconsistent highlighting for macro names
#7324 opened by ncfavier - 4
- 1
- 0
No warning about useless `{-# CATCHALL #-}` pragma
#7321 opened by andreasabel - 1
Normalization gives trivial `transp`
#7312 opened by Trebor-Huang - 6
Bad interaction between instance search and opaque
#7304 opened by UlfNorell - 0
Hard error on `instance` definition with unsolved type
#7286 opened by UlfNorell - 2
`--lossy-unification` doesn't fall back to regular unification when instances are used
#7289 opened by Thrithralas - 2
- 4
Agda >=2.6.3 hangs on conflicting record directives
#7301 opened by andreasabel - 6
with-abstraction regression
#7295 opened by UlfNorell - 0
- 4
- 4
Latex backend/package bug: `! Package array Error: Empty preamble: 'l' used.`
#7290 opened by WhatisRT - 12
fail in solving instance of `⊆-refl` in Agda 2.6.4.3
#7294 opened by mechvel - 2
Failed to write interface /usr/share/Agda-stdlib/_build/2.6.4.3/agda/src/Data/Unit/Base.agdai.
#7293 opened by juhp - 1
Recursion with records
#7291 opened by txa - 0
Compatibiilty of partial elements defined using cubical face lattice generators with reflextion machinery
#7288 opened by marcinjangrzybowski - 0
TBT: no termination error with `--double-check`
#7285 opened by andreasabel - 5
Internal error at Agda/TypeChecking/Substitute.hs:140:33
#7266 opened by kubaneko - 0
- 1
TBT: internal error in function `smallerOrEq`
#7279 opened by andreasabel - 2
`--no-syntax-based-termination` turns on `--type-based-termination`, but should not
#7269 opened by andreasabel - 0
TBT: no function nor calls listed in termination error
#7278 opened by andreasabel - 0
- 0
- 0
Named errors instead of Generic[Doc]Error
#7225 opened by andreasabel - 0
TBT accepts non-terminating function that makes Agda loop in the injectivity checker
#7272 opened by andreasabel - 3
--type-based-termination does not process postulates
#7267 opened by andreasabel - 0
TBT: Bug in size preservation regarding postulates
#7270 opened by andreasabel - 0
--type-based-termination: --size-preservation analysis comes too late for nested functions
#7268 opened by andreasabel - 2
Shape-irrelevance without-K broken by Agda 2.6.2
#7258 opened by andreasabel - 0
Error "This clause has target type ... which is not usable" highlights pattern instead of clause
#7262 opened by andreasabel - 0
Reexported instances lose overlap flags
#7250 opened by cmcmA20 - 24
semantically unjustified coinduction
#7220 opened by mikeshulman - 2
Internal error in opaque block when case splitting when just given extended lambda
#7218 opened by oskeri - 0
Release Agda 2.7.0
#7242 opened by jespercockx - 7
- 0
makefile hlint target needs cabal_macros.h
#7240 opened by philderbeast - 5
Expected a hidden argument, but found a visible argument in with-abstraction when using REWRITE
#7236 opened by sgodwincs - 1
- 2
Save-metas causes OOM during macro execution
#7227 opened by plt-amy - 2
OptionWarnings are emitted twice
#7221 opened by andreasabel - 4
`--double-check` fails in `TypeTopology` in the file `Naturals.Order` with version 2.6.4.3
#7217 opened by martinescardo - 0
No reproducer for error raised in `telePiPath`
#7226 opened by andreasabel - 0
Only warn about unknown warnings, don't fail hard
#7219 opened by andreasabel - 0
`agda-mode compile`: list of .el files might bitrot
#7215 opened by andreasabel - 1
Agda prints hidden function type in hidden argument as `{{...` and then fails to parse it
#7214 opened by andreasabel