-
Notifications
You must be signed in to change notification settings - Fork 367
Issues: agda/agda
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
ConstructorDoesNotFitInData error for record in Prop with Set fields
prop
Prop, definitional proof irrelevance
ux: error reporting
Issues to do with how Agda reports errors
The "latest" version of the documentation points to master
not-in-changelog
This issue should not be listed in the changelog.
ux: documentation
Issues relating to Agda's documentation
Should Agda optimise away the erasure from Vec to List?
backend: ghc
Haskell code generation backend ("MAlonzo")
type: discussion
Discussions about Agda's design and implementation
#7701
opened Feb 3, 2025 by
gallais
Feature request: Zero-indentation modules after the first
module
of a file
#7694
opened Jan 29, 2025 by
4e554c4c
Termination Checker Changes Decision Based on Dummy Argument
bug or feature?
It may be a bug, it may be a feature.
termination
Issues relating to the termination checker
#7693
opened Jan 28, 2025 by
NathanielB123
Option to completely disable generation of dot patterns
dot patterns
"Forced" (.x) patterns, wirtten by the user or generated by case splitting
type: enhancement
Issues and pull requests about possible improvements
ux: case splitting
Issues relating to the case split ("C-c C-c") command
ux: interaction
Issues to do with interactive development (holes, case splitting, etc)
Custom treeless pipeline is ignored for "recursive" calls
compiler-treeless
type: bug
Issues and pull requests about actual bugs
#7691
opened Jan 27, 2025 by
flupe
Out of memory when extracting witness from User question (not in changelog)
performance
Slow type checking, interaction, compilation or execution of Agda programs
with
Problems with the "with" abstraction
Dec
faq
#7690
opened Jan 26, 2025 by
noughtmare
Inductive identity allowed in negative position, inconsistent in Cubical Agda
cubical
Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp
false
Proof of the empty type which checks without known-unsafe flags (e.g. without --type-in-type)
positivity
Positivity checking for data-type definitions
Feature request: allow syntax which closes multiple parts over a common binder
syntax
Bike-shedding of the surface syntax
#7667
opened Dec 23, 2024 by
plt-amy
Agda ignores constructor parameters but only if they're copied under a parameterised module
pattern matching
Top-level pattern matching definitions, pattern matching in lets
#7664
opened Dec 20, 2024 by
plt-amy
[ question ] can we make Rewrite rules, rewrite rule matching
type: enhancement
Issues and pull requests about possible improvements
without-K
K-related restrictions to pattern matching, termination checking, indices, erasure
with-K
less infective/*definitional* on a per-data
declaration basis?
rewriting
#7663
opened Dec 20, 2024 by
jamesmckinna
Using Auto with a goal involving musical coinduction Coinductive records, musical coinduction
Mimer
Issue with the Mimer proof search engine
postfix-projections
Issue with projections in postfix form
regression in 2.7.0
♭
produces incorrect projection
coinduction
Add a warning for unresolved constructor name
overloading
Overloaded projections; Projection disambiguation
regression in 2.6.1
Regression that first appeared in Agda 2.6.1
type: enhancement
Issues and pull requests about possible improvements
ux: error reporting
Issues to do with how Agda reports errors
#7660
opened Dec 18, 2024 by
jespercockx
using ()
shouldn't import anything
import
Matching algorithm in rewriting does not reduce any pattern-matching definitions
faq
User question (not in changelog)
rewriting
Rewrite rules, rewrite rule matching
ux: documentation
Issues relating to Agda's documentation
#7654
opened Dec 12, 2024 by
L-TChen
Range Issues to do with interactive development (holes, case splitting, etc)
[ at 1.1-4 ]
printed without filename
range
ux: interaction
FOREIGN
is allowed when --safe
is on
backends
difficulty: easy
Internal error in Concerning internal errors of Agda
Mimer
Issue with the Mimer proof search engine
Agda/TypeChecking/Monad/Context.hs
using Mimer
internal-error
#7639
opened Dec 5, 2024 by
oskeri
Mimer implementation has Haskell coding style (not in changelog)
Ord
instances not compatible with Eq
style
#7638
opened Dec 4, 2024 by
andreasabel
Loss of context in Issue/PR stemming from AIM (Agda Implementor's Meeting)
forcing
Forcing analysis and forcing translation of clauses
reflection
Elaborator reflection, macros, tactic arguments
checkType
primitive
aim
#7630
opened Nov 29, 2024 by
WhatisRT
Internal error with src/full/Agda/TypeChecking/Substitute.hs:140:33 using Cubical Agda
cubical
Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp
internal-error
Concerning internal errors of Agda
Previous Next
ProTip!
Type g i on any issue or pull request to go back to the issue listing page.