My favorites ▼ | Sign in
Project Home Downloads Wiki Issues Source
New issue   Search
for
  Advanced search   Search tips
ListGrid
   
Loading...
  ID ▼ Type ▼ Status ▼ Priority ▼ Milestone ▼ Owner ▼   Summary + Labels ▼ ...
  659 Enhancement New ---- ---- ulf.nor...@gmail.com   Bad error message: "SetĪ‰ is not a valid type"  
  657 Defect Accepted High 2.3.2 ulf.nor...@gmail.com   Yet another display form problem  
  656 Defect Accepted High 2.3.2 ----   Pattern synonyms prevents caching  
  655 Enhancement New ---- ---- ----   Simple definitions should be a fine aliasing construct  
  652 Enhancement Accepted Medium ---- ----   Regression over 2.3.0: Failed to solve contraints ... blocked on problem ...  
  651 ---- InfoNeeded ---- ---- freli...@gmail.com   Agsy accepts a term that does not type-check afterwards.  
  649 ---- InfoNeeded ---- ---- ----   First file loaded into Agda-mode has no syntax highlighting  
  644 Enhancement InfoNeeded ---- ---- ulf.nor...@gmail.com   Another display form problem  
  641 Defect Accepted High 2.3.2 ----   Some OPTIONS pragmas are not reset when a buffer is reloaded  
  640 Defect Accepted High 2.3.2 nils.anders.danielsson   No highlighting after case-split  
  639 Defect Accepted High 2.3.2 ----   agda --ghci-interaction and agda --interaction-test should not silently ignore flags  
  638 Defect InfoNeeded High ---- a...@informatik.uni-muenchen.de   Incomprehensible error message caused by ElimView for a failed conversion check   Conversion  
  637 Defect Accepted Medium ---- nils.anders.danielsson   Out of stack/memory crashes should be reported properly in Emacs   Emacs Testsuite  
  635 Defect Accepted ---- ---- ulf.nor...@gmail.com   Case splitting emits things that should never be emitted!  
  632 Enhancement Accepted ---- ---- ulf.nor...@gmail.com   Printing of infix/mixfix operators defined in parametrized modules   Mixfix Syntax  
  630 Defect Accepted High ---- a...@informatik.uni-muenchen.de   _ printed for variable names [Goal: _]   Names Shadowing  
  627 Enhancement New Medium ---- a...@informatik.uni-muenchen.de   Let for irrefutable patterns   Syntax  
  625 Enhancement Accepted Medium ---- a...@informatik.uni-muenchen.de   Give accepts term with unsolvable metas   Meta Interaction  
  623 Defect Accepted Medium ---- ulf.nor...@gmail.com   Error message points to importing module rather than imported module   Modules  
  621 Defect Accepted High 2.3.2 nils.anders.danielsson   Slow syntax highlighting   Emacs  
  619 Enhancement Accepted ---- ---- nicolas....@gmail.com   Quote patterns   Reflection  
  615 Enhancement Accepted Medium ---- a...@informatik.uni-muenchen.de   Option (on by default?) to suppress printing of irrelevant terms   Irrelevance  
  608 Enhancement New ---- ---- a...@informatik.uni-muenchen.de   A refine command which just suggests a refinement  
  607 Defect Accepted Medium ---- a...@informatik.uni-muenchen.de   Projections not highlighted as such   Emacs  
  605 Enhancement New Medium ---- a...@informatik.uni-muenchen.de   show-goal-and-context does not include let-bindings   Interaction Emacs  
  604 Defect New Medium ---- a...@informatik.uni-muenchen.de   Refine shadows variable   Interaction  
  603 Enhancement Accepted ---- ---- ----   The dreaded != w and related error reporting  
  590 Enhancement Accepted Medium ---- nils.anders.danielsson   Emacs interaction: place cursor in new goal after successful tactic   Emacs  
  577 Defect Accepted Medium ---- nils.anders.danielsson   agda2-info changes focus when pop-frames is set to 't (or 'graphic-only)  
  576 Enhancement Accepted Medium ---- ----   There should be a well-defined and serached by default location for the standard library and user provided libraries.  
  575 Enhancement Accepted Medium ---- ----   Indenting lost on case-split   Interaction  
  573 Enhancement Accepted Medium ---- a...@informatik.uni-muenchen.de   Preserve ellipsis (...) when case splitting in interaction   Interaction  
  572 Enhancement New High ---- a...@informatik.uni-muenchen.de   Shadowed identifiers should be preceded by a dot when printed   Printing  
  570 Defect InfoNeeded Medium ---- a...@informatik.uni-muenchen.de   New mutual would require polarity annotation (computes polarity too late)  
  560 Enhancement InfoNeeded Medium ---- ----   Automatic "with" elimination  
  552 Defect Accepted Low ---- ulf.nor...@gmail.com   Pattern-matching fails to unify some implicit arguments  
  548 Defect Accepted High ---- makoto.t...@gmail.com   404 when Windows installer tries to download Emacs  
  547 Other New Medium ---- makoto.t...@gmail.com   Windows installer sources should be available  
  538 Enhancement InfoNeeded ---- ---- ----   Support cyclic module dependencies  
  536 Enhancement Accepted Medium ---- ----   Binding two identifiers using user-defined syntax  
  535 Enhancement Accepted High ---- ulf.nor...@gmail.com   case split on implicit argument could be better  
  534 Enhancement Accepted High ---- jmchap...@gmail.com   copy documentation from the release notes to the manual  
  532 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Support open public in record declarations, before field declarations  
  531 Defect Accepted Medium ---- JeanPhil...@gmail.com   Fixity and multipart operators don't mix smoothly  
  529 Enhancement InfoNeeded ---- ---- ulf.nor...@gmail.com   Specifying record parameters using record { ... } notation.  
  528 Defect Accepted Medium ---- ulf.nor...@gmail.com   Fixity declarations in records are applied too late.  
  526 Enhancement Accepted ---- ---- ulf.nor...@gmail.com   Don't just write _49, include the corresponding implicit variable name as well (if any)  
  525 Enhancement Accepted Medium ---- ----   Unification problem when a term's type is an implicit function   Meta  
  520 Enhancement Accepted Low ---- ----   rewrite can't handle x == f x equalities  
  516 Enhancement Accepted Low ---- ----   Feature request: show types of indicated terms.   Emacs  
  515 ---- InfoNeeded ---- ---- ----   A generative identity built-in (feature request)  
  514 Enhancement New ---- ---- ulf.nor...@gmail.com   Increase sharing of in-memory proof terms  
  513 Defect Accepted Medium ---- ulf.nor...@gmail.com   Case-spitting isn't aware that rewrite isn't supposed to be a with block  
  510 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Strange behavior with nested with clauses  
  508 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Support Bird-style literate Agda  
  500 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Allow creation of implicit parameters in with blocks  
  496 Enhancement New ---- ---- ulf.nor...@gmail.com   Turn abstract into "a block thing"  
  495 Enhancement Accepted Medium ---- adamgundry   Improve range info in pattern synonyms  
  493 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Accept using/hidden/renaming qualifiers on module opens in arbitrary orders  
  488 Defect Accepted Medium ---- ulf.nor...@gmail.com   Refining on user defined syntax mixes up the order of the subgoals   Emacs  
  487 Enhancement Accepted Medium ---- nicolas....@gmail.com   list literals and list comprehensions  
  481 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Let "open import" pass parameters to parametrized modules  
  480 Defect Accepted Medium ---- ulf.nor...@gmail.com   Postponing checking of left hand sides  
  471 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Emacs command to show goal with constraints on it   Emacs  
  470 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Constraint solving in heterogenous situations   Meta  
  466 Defect Accepted Medium ---- nicolas....@gmail.com   `unquote' does not play nicely with local bindings   Reflection  
  460 Enhancement InfoNeeded Low ---- a...@informatik.uni-muenchen.de   Keyword 'auto'  
  459 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Emacs command to generate helper function   Emacs  
  449 Enhancement Accepted Medium ---- nicolas....@gmail.com   Add pattern matching to reflection mechanisms  
  437 Enhancement Accepted Low ---- a...@informatik.uni-muenchen.de   Detect when something cannot be a function type   Meta  
  436 Defect Accepted Medium ---- ulf.nor...@gmail.com   Case splitting and pattern matching lambdas  
  434 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Make let expressions less restricted and/or provide better error messages for defined fields  
  433 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Local abstraction barriers  
  431 Defect Accepted Medium ---- ulf.nor...@gmail.com   Constructor-headed function makes type-checker diverge   Meta  
  426 Enhancement Accepted Medium ---- a...@informatik.uni-muenchen.de   Call-by-name makes linear program exponential   Performance  
  421 Enhancement Accepted Low ---- ulf.nor...@gmail.com   Higher order positivity  
  420 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Named arguments in module applications  
  408 Enhancement New Medium ---- a...@informatik.uni-muenchen.de   Order of clauses matters to much; equations should hold definitionally whenever possible.   Patternmatching  
  407 Enhancement Accepted Medium ---- a...@informatik.uni-muenchen.de   Syntax \ {x = x} for named hidden abstraction missing  
  402 Defect Accepted Medium ---- a...@informatik.uni-muenchen.de   Recursive records make Agda loop   Eta  
  400 Enhancement Accepted Low ---- JeanPhil...@gmail.com   syntax definitions expanding to hidden arguments   Syntax  
  394 Enhancement Accepted Medium ---- JeanPhil...@gmail.com   Mixfix binders with multi-variable lambdas does not parse  
  390 Defect Accepted Medium ---- Daniel.G...@gmail.com   Epic backend generates segfaulting program  
  387 Defect Accepted Medium ---- ulf.nor...@gmail.com   Shifted goals with hole in field type  
  378 Defect Accepted Low ---- freli...@gmail.com   Auto generates an invalid expression  
  376 Enhancement InfoNeeded Medium ---- a...@informatik.uni-muenchen.de   Expanding record variables during constraint solving   Eta Meta  
  370 Enhancement Accepted Medium ---- nils.anders.danielsson   SHARP generativity loses stability under substitution  
  361 Defect Accepted Low ---- a...@informatik.uni-muenchen.de   Printing records in eta-contracted form let them look ill-typed sometimes   Eta  
  359 Enhancement InfoNeeded Medium ---- ----   What should the rules for shadowing be?  
  351 Enhancement Accepted Medium ---- a...@informatik.uni-muenchen.de   Constraint solving for irrelevant metas   Irrelevance  
  339 Enhancement Accepted Low ---- ulf.nor...@gmail.com   Better vim syntax highlighting: here is the vim half  
  326 Enhancement Accepted Low ---- ulf.nor...@gmail.com   Optimise MAlonzo's primQNameEquality  
  325 Enhancement New Medium ---- a...@informatik.uni-muenchen.de   More agressive unification   Meta  
  319 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Split on multiple variables at once  
  318 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Bad error message (scope checker)   Scope  
  300 Defect Accepted Medium ---- a...@informatik.uni-muenchen.de   Size constraint solving broken for rank-2 size quantification  
  297 Enhancement Accepted Medium ---- ulf.nor...@gmail.com   Disallow shadowing of constructors in lambdas  
  289 Defect Accepted Medium ---- ulf.nor...@gmail.com   Case splitting in already instantiated hole   Emacs Meta  
  279 Defect Accepted High ---- ulf.nor...@gmail.com   Incorrect disambiguation of overloaded constructor  
  260 Enhancement New Medium ---- ulf.nor...@gmail.com   Ensure that everything has a unique name  
CSV
  
Show columns:
 ♦ ID
 ♦ Type
 ♦ Status
 ♦ Priority
 ♦ Milestone
 ♦ Owner
 ♦ Summary
    Attachments
    Stars
    Opened
    Closed
    Modified
    BlockedOn
    Blocking
    Blocked
    MergedInto
    Reporter
    Cc
    Project
    Pattern
    Sized
    Opsys
    Case
    Edit column spec...
Powered by Google Project Hosting