rocq-prover/equations

Issues somebody may already be working on are listed last. List everything by date

• Please add "rocq-equations.1.3.2+9.3" to the `released` opam archive.

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 1/5 Under an hour Newbie friendliness 68/100

  rocq-prover/equations#745 · Opened Oct 4, 2026

• Difference to fixpoints in catch-all/default branches leading to guard checker problems

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 48/100

  rocq-prover/equations#742 · Opened Sep 18, 2026

• Explicit argument is being shadowed by implicit argument

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 3/5 1-2 days Newbie friendliness 55/100

  rocq-prover/equations#741 · Opened Aug 27, 2026

• The link in repo description is invalid

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 2/5 1-3 hours Newbie friendliness 68/100

  rocq-prover/equations#731 · Opened Jul 21, 2026

• Using Equations yields 75x slowdown compared with structural recursion

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 45/100

  rocq-prover/equations#710 · 5 comments · Opened Apr 9, 2026

• Extensionality Tactic does not seem to be running the `Obligation Tactic` as implied by error message

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 48/100

  rocq-prover/equations#708 · 1 comment · Opened Mar 26, 2026

• No package compatible with rocq 9.2.dev

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 2/5 1-3 hours Newbie friendliness 55/100

  rocq-prover/equations#693 · 1 comment · 1 reaction · Opened Jan 23, 2026

• funelim of high order function using Type results in "Product do not match" error

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 35/100

  rocq-prover/equations#660 · Opened Jul 26, 2025

• Vernacular `Derive` conflicts with Rocq Derive feature

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 2/5 1-3 hours Newbie friendliness 35/100

  rocq-prover/equations#656 · 3 comments · Opened Jun 14, 2025

• Missing equality hypothesis in proof obligation?

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 35/100

  rocq-prover/equations#654 · 1 comment · Opened May 9, 2025

• Equations does not handle implicit constructor coercions in patterns

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 35/100

  rocq-prover/equations#647 · 1 comment · Opened Apr 9, 2025

• Bug in graph generation causes illegal application

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 35/100

  rocq-prover/equations#643 · Opened Mar 24, 2025

• Improve deplim etc...

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 25/100

  rocq-prover/equations#638 · 1 comment · Opened Feb 18, 2025

• Regression with Coq 8.20: ill-typed term with universe issue

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 38/100

  rocq-prover/equations#635 · 12 comments · Opened Jan 30, 2025

• Ill-typed term produced after name collision (?)

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 35/100

  rocq-prover/equations#634 · Opened Jan 30, 2025

• Equations picks constructor over local variable when resolving names

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 3/5 1-2 days Newbie friendliness 45/100

  rocq-prover/equations#629 · Opened Jan 8, 2025

• Importing Equations breaks std++'s 'simplify_eq' tactic

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 3/5 1-2 days Newbie friendliness 48/100

  rocq-prover/equations#628 · Opened Dec 5, 2024

• Function is more helpful than Equations

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 5/5 Over a week Newbie friendliness 15/100

  rocq-prover/equations#627 · Opened Dec 5, 2024

• Equations and Obligations

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 3/5 1-2 days Newbie friendliness 35/100

  rocq-prover/equations#624 · Opened Nov 18, 2024

• Bug: f_unfold obligation after Defined

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 35/100

  rocq-prover/equations#623 · 1 comment · Opened Nov 18, 2024

• Warning for inlining Signature for

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 5/5 Over a week Newbie friendliness 25/100

  rocq-prover/equations#622 · 4 comments · Opened Oct 8, 2024

• Deeplim inverses some equalities when sections are involved

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 38/100

  rocq-prover/equations#621 · 1 comment · Opened Oct 8, 2024

• Equations taking a long time to type check mutually recursive functions

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 5/5 Over a week Newbie friendliness 25/100

  rocq-prover/equations#620 · 1 comment · Opened Oct 7, 2024

• Anomaly "in Univ.repr: Universe file.v.1700 undefined."

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 35/100

  rocq-prover/equations#614 · Opened Aug 26, 2024

• Install/export module with inspect definition and notation like eqn

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 3/5 1-2 days Newbie friendliness 45/100

  rocq-prover/equations#613 · Opened Jul 11, 2024

• Limited support when the decreasing argument is a Prop while the return type is in Type

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 38/100

  rocq-prover/equations#598 · 1 comment · Opened May 16, 2024

• Crash with Coq 8.19

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 28/100

  rocq-prover/equations#583 · Opened Feb 28, 2024

• Generated elimination principle is missing some induction hypotheses

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 5/5 Over a week Newbie friendliness 35/100

  rocq-prover/equations#576 · 1 comment · 1 reaction · Opened Dec 22, 2023

• Documentation mentions non-existing symbols

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 2/5 1-3 hours Newbie friendliness 35/100

  rocq-prover/equations#575 · 1 comment · Opened Dec 22, 2023

• Potential Bug that crashes coqtop

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 30/100

  rocq-prover/equations#572 · Opened Nov 23, 2023

• Many links broken on http://mattam82.github.io/Coq-Equations/

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 3/5 1-2 days Newbie friendliness 35/100

  rocq-prover/equations#571 · 1 comment · Opened Nov 14, 2023

• Anomaly "in Univ.repr: Universe Var(0) undefined." with `Derive Signature NoConfusion EqDec for Var.`

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 35/100

  rocq-prover/equations#554 · Opened Jul 10, 2023

• Anomaly "in Univ.repr: Universe MetaCoq.SafeChecker.PCUICSafeConversion.12667 undefined." Please report at http://coq.inria.fr/bugs/

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 32/100

  rocq-prover/equations#545 · 2 comments · Opened Apr 5, 2023

• Hang / unlimited memory use with `simp` on trivial function not occurring in Goal

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 30/100

  rocq-prover/equations#538 · 1 comment · Opened Feb 14, 2023

• [feature request] Attributes #[transparent/opaque]

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 5/5 Over a week Newbie friendliness 15/100

  rocq-prover/equations#522 · Opened Dec 15, 2022

• Merely `Require Equations.Prop.Equations.` breaks the derive plugin shipped in Coq's standard library

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 3/5 1-2 days Newbie friendliness 35/100

  rocq-prover/equations#515 · Opened Oct 25, 2022

• Exception on invalid syntax

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 3/5 1-2 days Newbie friendliness 42/100

  rocq-prover/equations#508 · Opened Aug 24, 2022

• Notation conflict with standard library

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 25/100

  rocq-prover/equations#505 · 1 comment · Opened Jul 28, 2022

• Stack overflow with UIP

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 28/100

  rocq-prover/equations#498 · 2 comments · Opened Jul 12, 2022

• Subsume funind

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 25/100

  rocq-prover/equations#495 · 1 comment · Opened Jun 24, 2022

• Equations generates wrong variable names

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 38/100

  rocq-prover/equations#493 · Opened May 24, 2022

• Hang on funelim

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 35/100

  rocq-prover/equations#491 · Opened Apr 12, 2022

• Anomaly when using CoInductive types

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 5/5 Over a week Newbie friendliness 30/100

  rocq-prover/equations#490 · Opened Apr 11, 2022

• `funelim` with dependently typed function doesn't eliminate

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 42/100

  rocq-prover/equations#488 · Opened Apr 8, 2022

• Equations raises type error where Program generates proof obligation

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 35/100

  rocq-prover/equations#478 · Opened Mar 9, 2022

• Bug: Derive NoConfusion for this inductive seems almost correct, but forgets to apply an argument?

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 35/100

  rocq-prover/equations#441 · 1 comment · Opened Oct 23, 2021

• Support explicit naming of hypotheses generated by funelim

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 5/5 Over a week Newbie friendliness 25/100

  rocq-prover/equations#415 · 2 comments · Opened Jul 12, 2021

• Failure to derive NoConfusionHom

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 35/100

  rocq-prover/equations#414 · 1 comment · Opened Jul 11, 2021

• Anomaly when name mangling is enabled

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 4/5 3-5 days Newbie friendliness 25/100

  rocq-prover/equations#407 · 1 comment · Opened Jun 22, 2021

• #[tactic=tac] should apply to omitted cases

  Open

  ⋯Report a problem with this issue

  • Is something wrong?

  • Already taken
  • Not beginner-friendly
  • Stale or invalid
  • Something else…
  • Send Cancel

  Difficulty 5/5 Over a week Newbie friendliness 25/100

  rocq-prover/equations#402 · 3 comments · Opened Jun 11, 2021