Skip to content

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.

Sign up for GitHub

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

990 Open 4,568 Closed
990 Open 4,568 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Positivity checker doesn't respect definitional equality positivity Positivity checking for data-type definitions
#7669 opened Dec 25, 2024 by szumixie
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
#7668 opened Dec 25, 2024 by szumixie
1
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
Auto resorts to circular reasoning under a with-abstraction
#7665 opened Dec 21, 2024 by laserbat
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
8
[ question ] can we make with-K less infective/*definitional* on a per-data declaration basis? rewriting 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
#7663 opened Dec 20, 2024 by jamesmckinna
1
Using Auto with a goal involving musical coinduction ♭ produces incorrect projection
#7662 opened Dec 20, 2024 by jake-87
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
3
Using auto leads to __IMPOSSIBLE__ called at src/full/Agda/TypeChecking/Telescope.hs:681:24 when Σ and case_of_ are both present
#7659 opened Dec 18, 2024 by laserbat
1
using () shouldn't import anything import Issues to do with importing modules regression in 2.6.2 Regression that first appeared in Agda 2.6.2 type: bug Issues and pull requests about actual bugs
#7656 opened Dec 12, 2024 by andreasabel 2.8.0
@andreasabel
14
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
@L-TChen
11
Range [ at 1.1-4 ] printed without filename range ux: interaction Issues to do with interactive development (holes, case splitting, etc)
#7646 opened Dec 7, 2024 by andreasabel 2.8.0
@andreasabel
2
FOREIGN is allowed when --safe is on backends difficulty: easy Supposedly easy to fix. safe Subset of Agda features which is expected to be consistent
#7644 opened Dec 6, 2024 by nad 2.8.0
4
Panic: uncaught pattern violation internal-error Concerning internal errors of Agda regression in 2.6.3
#7643 opened Dec 6, 2024 by noughtmare 2.8.0
6
Internal error in Agda/TypeChecking/Monad/Context.hs using Mimer internal-error Concerning internal errors of Agda Mimer Issue with the Mimer proof search engine
#7639 opened Dec 5, 2024 by oskeri
9
Mimer implementation has Ord instances not compatible with Eq style Haskell coding style (not in changelog)
#7638 opened Dec 4, 2024 by andreasabel
Loss of context in checkType primitive aim Issue/PR stemming from AIM (Agda Implementor's Meeting) forcing Forcing analysis and forcing translation of clauses reflection Elaborator reflection, macros, tactic arguments
#7630 opened Nov 29, 2024 by WhatisRT
2
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
#7629 opened Nov 29, 2024 by anshwad10 2.8.0
1
Make it possible to run double-checker on definitions checkInternal Bugs with, or caught by, the internal double-checker pattern matching Top-level pattern matching definitions, pattern matching in lets type: enhancement Issues and pull requests about possible improvements type-checking
#7627 opened Nov 29, 2024 by liesnikov
@liesnikov
Make it possible to leave out implicit fields for copattern matches
#7626 opened Nov 29, 2024 by jashug
Internal Error involving reduction and instance arguments instance Instance resolution internal-error Concerning internal errors of Agda regression in 2.6.1 Regression that first appeared in Agda 2.6.1 ux: interaction Issues to do with interactive development (holes, case splitting, etc)
#7624 opened Nov 28, 2024 by jashug 2.8.0
@kubaneko
2
Problem supplying infix parameters to data declaration? data Inductive data definitions mixfix Interaction between mixfix operators and other language features operators Parsing of mixfix operators type: enhancement Issues and pull requests about possible improvements
#7620 opened Nov 25, 2024 by jamesmckinna icebox
7
Cubical: forcing affects termination-check cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp forcing Forcing analysis and forcing translation of clauses termination Issues relating to the termination checker
#7616 opened Nov 23, 2024 by andreasabel later
1
'Stacks': Level heterogeneous lists of Sets levels pattern matching Top-level pattern matching definitions, pattern matching in lets pattern-synonyms type: enhancement Issues and pull requests about possible improvements
#7614 opened Nov 21, 2024 by jamesmckinna later
2
No support for Arm64 Linux
#7603 opened Nov 4, 2024 by haohanyang
2
ProTip! Follow long discussions with comments:>50.