agda/agda issues and pull requests

#7508 - Unused-arg optimization breaks function call

Issue - State: open - Opened by lawcho 4 days ago
Labels: type: bug, backend: js

#7507 - Broken CI/haskell installation on GitHub?

Issue - State: open - Opened by jamesmckinna 4 days ago - 1 comment
Labels: build-failure, happy, upstream

#7506 - 2.7.0.1 missed on `https://wiki.portal.chalmers.se/agda/pmwiki.php`

Issue - State: closed - Opened by mechvel 5 days ago - 1 comment
Labels: ux: documentation, release

#7505 - Remove unused `clauseExact` field

Pull Request - State: open - Opened by szumixie 7 days ago
Labels: exact split, type: task

#7502 - Make termination checking more permissive wrt non-exact clause reduction

Pull Request - State: closed - Opened by szumixie 11 days ago - 2 comments
Labels: type: enhancement, termination, catch-all

#7491 - ES6 modules

Pull Request - State: open - Opened by lawcho 16 days ago - 7 comments
Labels: backend: js

#7489 - TypeChecking.Pretty: remove and change some SPECIALIZE pragmas

Pull Request - State: closed - Opened by andreasabel 18 days ago - 1 comment
Labels: performance, refactor

#7449 - Instances found by instance search are inlined

Issue - State: open - Opened by jespercockx about 1 month ago - 3 comments
Labels: performance, instance, bug or feature?

#7303 - Revert cyclic computation of ranges (and ban `mdo` from this code base)

Issue - State: open - Opened by andreasabel 4 months ago - 4 comments
Labels: range, refactor, Agda loops

#6975 - Expose the names of generated record constructors

Pull Request - State: open - Opened by plt-amy 11 months ago - 3 comments
Labels: record constructors

#3801 - Allow declarations in inner scopes to shadow declarations in outer scopes

Issue - State: open - Opened by andreasabel over 5 years ago - 6 comments
Labels: scope, shadowing, language change, ux: warnings

#100 - Small change to the meaning of open import

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 4 comments
Labels: type: enhancement

#99 - Preserve more ranges

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 3 comments
Labels: type: bug

#98 - Function doesn't type check with unclear error message

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#97 - Different behavior between an Agda file and an literate Agda file

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 6 comments
Labels: type: bug

#96 - Easier way to bring data type with all constructors into scope

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 15 comments
Labels: type: enhancement, modules, syntax

#95 - Shallow injectivity inference brittle?

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#94 - Panic: : no such name dummy

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#93 - Emacs mode with others input methods doesn't work

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 4 comments
Labels: type: bug

#92 - The compiler chokes on certain module names

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#91 - Constructors are not highlighted in with clauses

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#90 - Improve the "Set != Set1" error message

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: enhancement

#89 - The normaliser stops too early

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#88 - Compiler should check that file name matches module name

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#87 - Binding previously dotted variable in with-clause

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 3 comments
Labels: type: bug

#86 - Incorrect ranges on overloaded constructors

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#85 - open renaming

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 4 comments
Labels: type: bug

#84 - Problem with ~ + with + ()

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#83 - Using ~ in a name part

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#82 - Poor error message ("[...] internal error [...] GHC [...]")

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 4 comments
Labels: type: bug

#81 - Overzealous splitting (or bug in the coverage checker)

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#80 - Internal error (with)

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#79 - Magic disambiguation of overloaded constructor

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 12 comments
Labels: type: enhancement, type-checking, overloading

#78 - Proper support for @-patterns

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 3 comments
Labels: type: enhancement, pattern matching, as-patterns

#77 - eta for records not working (possibly)

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#76 - Parentheses missing in output from case-split

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 4 comments
Labels: type: bug

#75 - Sometimes hidden arguments cannot be referenced by name

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 3 comments
Labels: type: bug

#74 - Case-splitting does not work in modules with hidden parameters

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#73 - () should not be printed in dotted patterns

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 3 comments
Labels: type: bug

#72 - Problem with make-case + with

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#71 - [deleted issue]

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago

#70 - The impossible happened

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 4 comments
Labels: type: bug

#69 - Indirectly-imported constructors gratuitously qualified in normalization output

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#68 - Standard library uses rare unicode characters, can't find font to use with PuTTY for them...

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#67 - Memory leak in the emacs mode

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 5 comments
Labels: type: bug

#66 - Data.DifferenceList.[] is not implemented correctly

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 3 comments
Labels: type: bug

#65 - Emacs mode does not give any feedback with an incorrect @

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#64 - Names not displayed properly when open public is used

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 4 comments
Labels: type: enhancement

#63 - A data type can have two constructors with the same name

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#62 - Constructor can be used when not in scope

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 4 comments
Labels: type: bug

#61 - Compilation fails with the darcs sources

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#60 - open public in record fails

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#59 - Improving termination checking of functions defined using with

Issue - State: open - Opened by GoogleCodeExporter about 9 years ago - 36 comments
Labels: type: enhancement, termination, with, help wanted

#58 - Termination checker fails because of hidden argument

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#57 - Panic (as pattern in with clause)

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug, with, as-patterns

#56 - x@p is not an instance of x@p

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 3 comments
Labels: type: bug

#55 - Panic: overloaded constructors and open public

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 3 comments
Labels: type: bug

#54 - More coverage checker panic

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#53 - The termination checker does not handle all dotted patterns correctly

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#52 - Coverage checker impossibility

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#51 - RHS accepted for impossible LHS

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#50 - Coverage checker panic

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#49 - Named arguments don't work for module parameters

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#48 - agda -I does not warn about unsolved meta-variables

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#47 - Refine adds a prime (') to some variable names

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 3 comments
Labels: type: bug

#46 - Togglin the --no-coverage-check flag is not working in emacs

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#45 - computation gives up in mutual definition

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 6 comments
Labels: type: enhancement

#44 - more clever lifting of local functions

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 4 comments
Labels: type: enhancement, modules, unused-arguments, polarity

#43 - Can't build Agda 2.1.2 on Ubuntu Gutsy

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#42 - Interleaving type checking and termination checking

Issue - State: open - Opened by GoogleCodeExporter about 9 years ago - 11 comments
Labels: type: enhancement

#41 - Incomprehensible error message related to open in let

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#40 - Reusing field names does not always work

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#39 - The impossible happened

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#38 - Strange behaviour of open import public renaming

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#37 - Eta expansion is not performed before "magic with" abstraction

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 3 comments
Labels: type: bug

#36 - Two definitions with the same name can be exported from a module

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 3 comments
Labels: type: enhancement

#35 - No scope checking of fixity declarations in records

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#34 - Instantiating modules in a record declaration does not quite work

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 4 comments
Labels: type: bug

#33 - funny error message

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#32 - end of file during parsing

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 5 comments
Labels: type: bug

#31 - A name leaks into scope

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#30 - How much shadowing should be allowed?

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 6 comments
Labels: type: enhancement

#29 - stack overflow

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 8 comments
Labels: type: bug

#28 - new record syntax doesn't work with emacs mode

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#27 - Can not refine

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#26 - pattern matching against natural number literals

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug, pattern matching, literals

#25 - pragma suppresses shed

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#24 - hidden lambda's inserted before interaction metas

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#23 - Literate agda files are not working

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#22 - working with records

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#21 - Agda crashes on poorly formatted interface files

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#20 - Pragmas are too static in the GUI

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 3 comments
Labels: type: bug

#19 - parsing error when using ¡

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#18 - postulate keyword is not considered in the layout

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#17 - strange scoping over with

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

#16 - disabling termination checking for specific functions

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 3 comments
Labels: type: enhancement, termination

#15 - goal recognition is a bit hit and miss

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 5 comments
Labels: type: bug

#14 - Agda's exit code should be non-zero when termination checking fail

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 2 comments
Labels: type: bug

#13 - prettyTCM loops

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 4 comments
Labels: type: bug

#12 - unbound variable exception with verbosity 9

Issue - State: closed - Opened by GoogleCodeExporter about 9 years ago - 1 comment
Labels: type: bug

GitHub / agda/agda issues and pull requests