Topics:
- Accessing where clauses as independent functions (23 messages, latest: Dec 08 2022 at 11:01)
- Program (2 messages, latest: Dec 06 2022 at 12:05)
- Why are `where` clause obligations reversed? (1 message, latest: Nov 15 2022 at 19:50)
- Syntax of `with` (7 messages, latest: Nov 11 2022 at 20:09)
- Support for Coinductive data (2 messages, latest: Oct 11 2022 at 19:07)
- Derive NoConfusionHom for an eq-like type (2 messages, latest: Sep 21 2022 at 16:28)
- ✔ Licensing issues (2 messages, latest: Sep 20 2022 at 10:14)
- getting equalities out of with clauses (22 messages, latest: Sep 07 2022 at 13:04)
- Equations for 8.16? (3 messages, latest: Aug 17 2022 at 11:51)
- funelim slow (3 messages, latest: Aug 11 2022 at 10:16)
- Derive EqDec for parametrised types (10 messages, latest: Jul 26 2022 at 08:46)
- Use `with` matching conditions when proving obligations (3 messages, latest: Jul 20 2022 at 14:32)
- Cannot define tree_eqdec mutally with other programs (5 messages, latest: Jul 13 2022 at 14:08)
- ✔ Possible Bug in Equations Package, but I could be wrong. (24 messages, latest: Jun 19 2022 at 07:36)
- Termination with higher-order functions (8 messages, latest: May 24 2022 at 09:20)
- ✔ Not finding a NoConfusion? (6 messages, latest: May 18 2022 at 16:46)
- New user feedback (5 messages, latest: May 08 2022 at 08:37)
- stream events (3 messages, latest: May 02 2022 at 08:40)
- Compatibility with ssreflect (2 messages, latest: Apr 15 2022 at 09:02)
- Equations type error on `fin t` while `Program` does not (4 messages, latest: Mar 10 2022 at 14:53)
- `with` on `with` (27 messages, latest: Mar 03 2022 at 15:48)
- Equations simultaneous `with` (10 messages, latest: Mar 02 2022 at 14:22)
- ✔ Don't simplify obligations (27 messages, latest: Mar 01 2022 at 13:19)
- Derive NoConfusion Anomaly (7 messages, latest: Feb 25 2022 at 09:52)
- Derive NoConfusion failing (23 messages, latest: Feb 02 2022 at 15:56)
- Transparency as an attribute (2 messages, latest: Dec 15 2021 at 16:24)
- ✔ coq-equations "not found in table: equations.fixproto" (11 messages, latest: Nov 30 2021 at 18:51)
- 1.3 for 8.13? (7 messages, latest: Nov 26 2021 at 10:34)
- Solve Obligations tactic returned error: Proof is not com... (10 messages, latest: Nov 25 2021 at 19:09)
- deep pattern matching and recursive guards (11 messages, latest: Oct 28 2021 at 15:55)
- 8.14 branch compatibility? (3 messages, latest: Sep 25 2021 at 12:42)
- Weird syntax error with `by struct` (9 messages, latest: Jun 09 2021 at 10:10)
- Equations incompatible with mathematical components? (6 messages, latest: May 27 2021 at 10:43)
- mutual recursion leaving an obligation for _graph_correct (53 messages, latest: May 10 2021 at 12:08)
- `noconf` in goal (5 messages, latest: Apr 20 2021 at 18:58)
- Noob question about decreasing argument (4 messages, latest: Apr 01 2021 at 15:46)
- apply_funelim vs funelim (5 messages, latest: Jan 04 2021 at 13:13)
- New release for Coq 8.13 (5 messages, latest: Dec 18 2020 at 17:51)
- Case splitting trouble (15 messages, latest: Nov 30 2020 at 12:33)
- eq_refl arguments in Equations.Prop (10 messages, latest: Nov 18 2020 at 13:53)
- Equations intro (3 messages, latest: Nov 13 2020 at 13:29)
- Can where definitions make recursive calls in a with node? (3 messages, latest: Oct 01 2020 at 22:12)
- Obligation abstracting over unnecessary section variables (23 messages, latest: Jul 04 2020 at 21:37)
- Address all obligations at once (3 messages, latest: Jul 03 2020 at 10:53)
- Derive EqDec failing silently (6 messages, latest: Jun 23 2020 at 12:40)
- Equations in an abstract setting (6 messages, latest: Jun 12 2020 at 10:09)
- Computing with well founded recursion (14 messages, latest: Jun 10 2020 at 17:31)
- imported from gitter room coq/Equations (328 messages, latest: Apr 23 2020 at 16:41)
Last updated: Dec 09 2022 at 09:30 UTC