Skip to content

Issues: mattam82/Coq-Equations

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

66 Open 162 Closed
66 Open 162 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
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

Limited support when the decreasing argument is a Prop while the return type is in Type
#598 opened May 16, 2024 by HuStmpHrrr
1
Anomaly "splitting Equations missing constraints in (anonymous)"
#597 opened May 14, 2024 by henriquebg99
Crash with Coq 8.19
#583 opened Feb 28, 2024 by jjhugues
Warnings can't be unset
#580 opened Jan 24, 2024 by YaZko
Failure to prove functional induction
#577 opened Dec 22, 2023 by terencode
Generated elimination principle is missing some induction hypotheses
#576 opened Dec 22, 2023 by RalfJung
Documentation mentions non-existing symbols
#575 opened Dec 22, 2023 by RalfJung
1
Potential Bug that crashes coqtop
#572 opened Nov 23, 2023 by Agnishom
Many links broken on http://mattam82.github.io/Coq-Equations/
#571 opened Nov 14, 2023 by jaccokrijnen
1
List.chop throws an exception when a recursive call is missing a parameter
#555 opened Jul 25, 2023 by agrn
Anomaly "in Univ.repr: Universe Var(0) undefined." with Derive Signature NoConfusion EqDec for Var.
#554 opened Jul 10, 2023 by SkySkimmer
Anomaly "in Univ.repr: Universe MetaCoq.SafeChecker.PCUICSafeConversion.12667 undefined." Please report at http://coq.inria.fr/bugs/
#545 opened Apr 5, 2023 by JasonGross
2
Hang / unlimited memory use with simp on trivial function not occurring in Goal
#538 opened Feb 14, 2023 by MSoegtropIMC
1
[feature request] Attributes #[transparent/opaque]
#522 opened Dec 15, 2022 by mattam82
Merely Require Equations.Prop.Equations. breaks the derive plugin shipped in Coq's standard library
#515 opened Oct 25, 2022 by JasonGross
Exception on invalid syntax
#508 opened Aug 24, 2022 by TobiasKappe
Notation conflict with standard library
#505 opened Jul 28, 2022 by jwiegley
1
Stack overflow with UIP
#498 opened Jul 12, 2022 by laMudri
2
Subsume funind
#495 opened Jun 24, 2022 by Alizter
1
Equations generates wrong variable names
#493 opened May 24, 2022 by fkj
Hang on funelim
#491 opened Apr 12, 2022 by Tuplanolla
Anomaly when using CoInductive types
#490 opened Apr 11, 2022 by euisuny
funelim with dependently typed function doesn't eliminate
#488 opened Apr 8, 2022 by Lysxia
Equations raises type error where Program generates proof obligation
#478 opened Mar 9, 2022 by elefthei
Bug: Derive NoConfusion for this inductive seems almost correct, but forgets to apply an argument?
#441 opened Oct 23, 2021 by drcicero
1
ProTip! Mix and match filters to narrow down what you’re looking for.