Topics:
- Subterm obligations (11 messages, latest: Sep 05 2023 at 19:55)
- ✔ Subterm obligations (2 messages, latest: Sep 04 2023 at 07:31)
- Installing coq-equations with coq.inria.fr down (3 messages, latest: Aug 14 2023 at 19:43)
- wf recursion with inductive vs. fixpoint (6 messages, latest: Jun 19 2023 at 09:14)
- working with subset types (7 messages, latest: Jun 12 2023 at 17:57)
- cannot guess decreasing argument (65 messages, latest: Apr 25 2023 at 09:38)
- `funelim` overflow and function extensionality (16 messages, latest: Apr 20 2023 at 14:14)
- Prodn map2 (4 messages, latest: Apr 14 2023 at 09:17)
- Denotational Semantics for Structs (7 messages, latest: Mar 25 2023 at 03:01)
- Recursive definition is ill-formed. (8 messages, latest: Mar 07 2023 at 04:43)
- The variable was not found (6 messages, latest: Mar 03 2023 at 19:30)
- Install from source error (5 messages, latest: Feb 09 2023 at 17:53)
- Placeholder Variable Naming Conventions (11 messages, latest: Feb 06 2023 at 16:36)
- Coq equtions is very very slow (12 messages, latest: Jan 17 2023 at 17:45)
- ✔ Coq equation's equivalent of `Set Program Cases` (18 messages, latest: Jan 12 2023 at 13:05)
- 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: Sep 23 2023 at 14:01 UTC