List view

MAlonzo does not properly clean up old builds

backend: ghcHaskell code generation backend ("MAlonzo")Haskell code generation backend ("MAlonzo")

status: MWE needed

Status: Open.

#5694 In agda/agda;

· andrewufrank opened on Dec 13, 2021

Resolving the monad instance for do notation

do notationChecking and desuraging of do notation, idiom brackets, matching in `do` blocksChecking and desuraging of do notation, idiom brackets, matching in `do` blocks

instanceInstance resolutionInstance resolution

type: discussionDiscussions about Agda's design and implementationDiscussions about Agda's design and implementation

Status: Open.

#4339 In agda/agda;

· berndlosert opened on Dec 30, 2019

Sometimes an outdated binary is not overwritten

backend: ghcHaskell code generation backend ("MAlonzo")Haskell code generation backend ("MAlonzo")

type: bugIssues and pull requests about actual bugsIssues and pull requests about actual bugs

Status: Open.

#3985 In agda/agda;

· nad opened on Aug 13, 2019

Emacs’ keyboard macros and Agda input method

agda-modeIssues relating to the Emacs agda2-modeIssues relating to the Emacs agda2-mode

help wanted

ux: emacsIssues relating to the Emacs agda2-modeIssues relating to the Emacs agda2-mode

Status: Open.

#3994 In agda/agda;

· guillaumebrunerie opened on Aug 15, 2019

Inefficient normalisation

call-by-namePerformance or correctness bugs with call-by-name (rather than by-need) evaluationPerformance or correctness bugs with call-by-name (rather than by-need) evaluation

parametersModule parametersModule parameters

performanceSlow type checking, interaction, compilation or execution of Agda programsSlow type checking, interaction, compilation or execution of Agda programs

reduction

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

whereProblems with where clausesProblems with where clauses

Status: Open.

#4036 In agda/agda;

· nad opened on Aug 26, 2019

confluence checker fails to notice obviously unsolvable constraints imply non-overlap of equations

rewritingRewrite rules, rewrite rule matchingRewrite rules, rewrite rule matching

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

Status: Open.

#4033 In agda/agda;

· JasonGross opened on Aug 24, 2019

Cannot split on argument even though goal type is inductive

copatternsDefinitions by copattern matching: projections on the LHSDefinitions by copattern matching: projections on the LHS

pattern matchingTop-level pattern matching definitions, pattern matching in letsTop-level pattern matching definitions, pattern matching in lets

reduction

type: bugIssues and pull requests about actual bugsIssues and pull requests about actual bugs

ux: case splittingIssues relating to the case split ("C-c C-c") commandIssues relating to the case split ("C-c C-c") command

Status: Open.

#3980 In agda/agda;

· gallais opened on Aug 9, 2019

Add support for inline do-notations

do notationChecking and desuraging of do notation, idiom brackets, matching in `do` blocksChecking and desuraging of do notation, idiom brackets, matching in `do` blocks

layoutRelated to layout-sensitive parsing.Related to layout-sensitive parsing.

parserProblems with the parser's implementation (rather than with decisions about syntax)Problems with the parser's implementation (rather than with decisions about syntax)

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

Status: Open.

#3935 In agda/agda;

· gallais opened on Jul 22, 2019

Out of order code block in literate mode

literate-agda

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

Status: Open.

#3885 In agda/agda;

· gallais opened on Jul 4, 2019

Hygienic macros?

reflectionElaborator reflection, macros, tactic argumentsElaborator reflection, macros, tactic arguments

type: discussionDiscussions about Agda's design and implementationDiscussions about Agda's design and implementation

Status: Open.

#3819 In agda/agda;

· nad opened on May 29, 2019

Problematic output when an operator constructor that was not originally declared as an operator is split

operatorsParsing of mixfix operatorsParsing of mixfix operators

type: bugIssues and pull requests about actual bugsIssues and pull requests about actual bugs

ux: case splittingIssues relating to the case split ("C-c C-c") commandIssues relating to the case split ("C-c C-c") command

ux: printingIssues relating to how terms are printed for displayIssues relating to how terms are printed for display

Status: Open.

#3797 In agda/agda;

· nad opened on May 22, 2019

Implement Language Server Protocol (LSP)

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

usabilityIssue affecting usability of Agda (UX: User eXperience)Issue affecting usability of Agda (UX: User eXperience)

ux: interactionIssues to do with interactive development (holes, case splitting, etc)Issues to do with interactive development (holes, case splitting, etc)

Status: Open.

#3758 In agda/agda;

· rwe opened on May 9, 2019

Proper support for inductive families in Cubical Agda

cubicalCubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transpCubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

Status: Open.

#3733 In agda/agda;

· nad opened on Apr 30, 2019

Add a universe of strict hSets

pattern matchingTop-level pattern matching definitions, pattern matching in letsTop-level pattern matching definitions, pattern matching in lets

propProp, definitional proof irrelevanceProp, definitional proof irrelevance

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

without-KK-related restrictions to pattern matching, termination checking, indices, erasureK-related restrictions to pattern matching, termination checking, indices, erasure

Status: Open.

#3397 In agda/agda;

· guillaumebrunerie opened on Nov 15, 2018

Erase elements of propositions from the memory

performanceSlow type checking, interaction, compilation or execution of Agda programsSlow type checking, interaction, compilation or execution of Agda programs

propProp, definitional proof irrelevanceProp, definitional proof irrelevance

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

Status: Open.

#3510 In agda/agda;

· guillaumebrunerie opened on Jan 18, 2019

Literate \begin{code}[hide] doesn't work with --html --html-highlight=code

literate-agda

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

Status: Open.

#3630 In agda/agda;

· martinescardo opened on Mar 14, 2019

Allow DISPLAY to check whether a lambda is constant

display pragmaIssues with the DISPLAY pragmaIssues with the DISPLAY pragma

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

ux: displayIssues relating to how terms are printed for displayIssues relating to how terms are printed for display

Status: Open.

#3585 In agda/agda;

· gallais opened on Feb 22, 2019

Infer the RHS of a "missing" clause by unification

cubicalCubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transpCubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp

recordsRecord declarations, literals, constructors and updatesRecord declarations, literals, constructors and updates

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

Status: Open.

#3576 In agda/agda;

· gallais opened on Feb 18, 2019

Misleading error messages in mutual definitions.

copatternsDefinitions by copattern matching: projections on the LHSDefinitions by copattern matching: projections on the LHS

mutual

parserProblems with the parser's implementation (rather than with decisions about syntax)Problems with the parser's implementation (rather than with decisions about syntax)

scopeIssues relating to scope checkingIssues relating to scope checking

Status: Open.

#3499 In agda/agda;

· semenov-vladyslav opened on Jan 13, 2019

Difference between con and def in reflection, and projections for records

reflectionElaborator reflection, macros, tactic argumentsElaborator reflection, macros, tactic arguments

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

Status: Open.

#3552 In agda/agda;

· guillaumebrunerie opened on Feb 9, 2019

Emacs : Display type of a subexpression.

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

ux: interactionIssues to do with interactive development (holes, case splitting, etc)Issues to do with interactive development (holes, case splitting, etc)

Status: Open.

#3502 In agda/agda;

· xekoukou opened on Jan 15, 2019

Add folding code for html backend

backend: htmlHTML generation backendHTML generation backend

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

Status: Open.

#3535 In agda/agda;

· gallais opened on Feb 1, 2019

Add blockIfConstraints?

reflectionElaborator reflection, macros, tactic argumentsElaborator reflection, macros, tactic arguments

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

Status: Open.

#3496 In agda/agda;

· nad opened on Jan 10, 2019

Memory issue with caching and highlighting

cachingRecompilation avoidance, interface filesRecompilation avoidance, interface files

performanceSlow type checking, interaction, compilation or execution of Agda programsSlow type checking, interaction, compilation or execution of Agda programs

ux: highlightingIssues relating to syntax highlightingIssues relating to syntax highlighting

Status: Open.

#1929 In agda/agda;

· UlfNorell opened on Apr 12, 2016

Do not fall back to pattern match for rewrite as rewrite is not a syntactic sugar anymore

rewriteThe "rewrite" construction in LHS-esThe "rewrite" construction in LHS-es

type: bugIssues and pull requests about actual bugsIssues and pull requests about actual bugs

ux: case splittingIssues relating to the case split ("C-c C-c") commandIssues relating to the case split ("C-c C-c") command

ux: interactionIssues to do with interactive development (holes, case splitting, etc)Issues to do with interactive development (holes, case splitting, etc)

Status: Open.

#2087 In agda/agda;

· ghost opened on Jul 7, 2016