List view

List of unicode bindings (in agda.sty?)

backend: latexLaTeX generation backendLaTeX generation backend

unicode

Status: Open.

#3645 In agda/agda;

· MatthewDaggitt opened on Mar 22, 2019

Treat metas coming from generalisable variables as neutral?

generalizeRelated to generalisable variablesRelated to generalisable variables

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

Status: Open.

#3671 In agda/agda;

· nad opened on Mar 31, 2019

Omit path-constructor corrections for transp when possible.

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

status: info-neededMore information is needed from the bug reporter to confirm the issue.More information is needed from the bug reporter to confirm the issue.

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

Status: Open.

#3675 In agda/agda;

· Saizan opened on Apr 2, 2019

Documentation of computational behaviour of cubical primitives

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

ux: documentationIssues relating to Agda's documentationIssues relating to Agda's documentation

Status: Open.

#3693 In agda/agda;

· nad opened on Apr 12, 2019

Allow declarations in inner scopes to shadow declarations in outer scopes

language changeChanges to the language which can be observed by Agda's userbaseChanges to the language which can be observed by Agda's userbase

scopeIssues relating to scope checkingIssues relating to scope checking

shadowingProblems caused by re-using names in the surface syntaxProblems caused by re-using names in the surface syntax

ux: warningsIssues relating to the reporting of warningsIssues relating to the reporting of warnings

Status: Open.

#3801 In agda/agda;

· andreasabel opened on May 23, 2019

More links could be named

backend: htmlHTML generation backendHTML generation backend

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

Status: Open.

#2735 In agda/agda;

· nad opened on Sep 6, 2017

Links to comments rather than code

backend: htmlHTML generation backendHTML generation backend

help wanted

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

Status: Open.

#3198 In agda/agda;

· nad opened on Aug 27, 2018

Single clause marked unreachable

coveragePattern-matching coverage checkerPattern-matching coverage checker

regression in 2.5.3Regression that first appeared in Agda 2.5.3Regression that first appeared in Agda 2.5.3

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

unreachable-clause

ux: warningsIssues relating to the reporting of warningsIssues relating to the reporting of warnings

Status: Open.

#3968 In agda/agda;

· andreasabel opened on Aug 7, 2019

Public open import in parametrised module wrongly reparametrises non parametrised definition

language changeChanges to the language which can be observed by Agda's userbaseChanges to the language which can be observed by Agda's userbase

modulesIssues relating to the module systemIssues relating to the module system

open-public

parametersModule parametersModule parameters

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

Status: Open.

#4057 In agda/agda;

· gallais opened on Sep 5, 2019

Provide interaction id's precise range

interaction-jsonJSON protocol for communicating with AgdaJSON protocol for communicating with Agda

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

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

Status: Open.

#4209 In agda/agda;

· ice1000 opened on Nov 18, 2019

Wrong context for solved interaction point in generalized type

generalizeRelated to generalisable variablesRelated to generalisable variables

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

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

Status: Open.

#4228 In agda/agda;

· UlfNorell opened on Nov 22, 2019

Architectural problem: unhygienic import handling, lack of sandboxing

importIssues to do with importing modulesIssues to do with importing modules

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

Status: Open.

Bug

#4272 In agda/agda;

· andreasabel opened on Dec 8, 2019

agda-mode: generate function template from type signature

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

difficulty: easySupposedly easy to fix.Supposedly easy to fix.

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

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

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

Status: Open.

#4294 In agda/agda;

· gallais opened on Dec 16, 2019

Split the codebase to a number of local packages

refactorChanges to the code base which do not affect users (not in changelog)Changes to the code base which do not affect users (not in changelog)

type: taskConcerning the development of Agda (not in changelog)Concerning the development of Agda (not in changelog)

Status: Open.

#4359 In agda/agda;

· L-TChen opened on Jan 8, 2020

Make checkInternal aware of --cubical

checkInternalBugs with, or caught by, the internal double-checkerBugs with, or caught by, the internal double-checker

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

type: taskConcerning the development of Agda (not in changelog)Concerning the development of Agda (not in changelog)

Status: Open.

#4455 In agda/agda;

· Saizan opened on Feb 18, 2020

Cannot use generalized variable in module application

generalizeRelated to generalisable variablesRelated to generalisable variables

modulesIssues relating to the module systemIssues relating to the module system

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

Status: Open.

#4489 In agda/agda;

· jespercockx opened on Feb 29, 2020

Unnecessary conversion checking due to parameterized module slows type-checking (a lot)

instanceInstance resolutionInstance resolution

modulesIssues relating to the module systemIssues relating to the module system

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

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

Status: Open.

#4517 In agda/agda;

· ajrouvoet opened on Mar 17, 2020

Slow typechecking unless using abstract in cubical

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

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

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

Status: Open.

#4573 In agda/agda;

· ayberkt opened on Apr 9, 2020

Weird variable .patternInTele0 showing up in goal

pattern binderIssues with record patterns in binders.Issues with record patterns in binders.

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

Status: Open.

#4599 In agda/agda;

· andreasabel opened on Apr 16, 2020

Should the GHC backend support Cabal and/or Stack?

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

help wanted

status: info-neededMore information is needed from the bug reporter to confirm the issue.More information is needed from the bug reporter to confirm the issue.

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

Status: Open.

#4627 In agda/agda;

· nad opened on Apr 29, 2020

Ensure portability of top-level module names (case-sensitivity)?

file systemInteractions between Agda's module system and the actual OS file systemInteractions between Agda's module system and the actual OS file system

top-level module

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

Status: Open.

#4678 In agda/agda;

· andreasabel opened on May 26, 2020

Record expressions do not respect renaming of fields

language changeChanges to the language which can be observed by Agda's userbaseChanges to the language which can be observed by Agda's userbase

names

record expressionIssues concerning record{...} expressions (record literals and record updates)Issues concerning record{...} expressions (record literals and record updates)

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

Status: Open.

#4720 In agda/agda;

· jespercockx opened on Jun 3, 2020

Since 2.5.4, Agda parses ordinary patterns after ellipsis

ellipsisIssues with the ellipsis (...) patternIssues with the ellipsis (...) pattern

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

regression in 2.5.4Regression that first appeared in Agda 2.5.4Regression that first appeared in Agda 2.5.4

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

Status: Open.

#4723 In agda/agda;

· andreasabel opened on Jun 3, 2020

cubical primitives should preserve guardedness

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

guardednessProblems of the guardedness checker for coinduction.Problems of the guardedness checker for coinduction.

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

Status: Open.

#4740 In agda/agda;

· txa opened on Jun 8, 2020

Deprecating primFloatToWord64

builtinEnhancements to the builtin modules and builtin definitionsEnhancements to the builtin modules and builtin definitions

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

Status: Open.

#4890 In agda/agda;

· wenkokke opened on Aug 30, 2020