Topics:
- ✔ Declare UIP for a specific instance ? (1 message, latest: Oct 08 2024 at 13:55)
- ✔ depelim does symmetry ? (2 messages, latest: Oct 08 2024 at 13:55)
- Warning Equations derive Signature (3 messages, latest: Oct 08 2024 at 13:52)
- What is the point of NoConfusion ? (16 messages, latest: Oct 08 2024 at 12:47)
- depelim does symmetry ? (2 messages, latest: Oct 08 2024 at 12:43)
- Difference noconf H et depelim H (3 messages, latest: Oct 08 2024 at 12:42)
- Declare UIP for a specific instance ? (2 messages, latest: Oct 08 2024 at 12:42)
- Products do not match error (3 messages, latest: Oct 01 2024 at 13:05)
- ✔ Trying out Equations before release (1 message, latest: Sep 23 2024 at 22:56)
- Trying out Equations before release (27 messages, latest: Sep 23 2024 at 15:14)
- Difference NoConfusion and NoConfusionHom (9 messages, latest: Sep 22 2024 at 22:06)
- ✔ Elimination of impossible branches (10 messages, latest: Sep 20 2024 at 13:10)
- Elimination of impossible branches (4 messages, latest: Sep 20 2024 at 13:00)
- Modification of funelim part of Platform 8.19 (3 messages, latest: Sep 20 2024 at 07:43)
- Equations renames hypothesis ??? (2 messages, latest: Sep 20 2024 at 07:41)
- Unable to automatically prove functional induction (4 messages, latest: Sep 18 2024 at 18:49)
- Overcoming inability to build a covering (3 messages, latest: Sep 05 2024 at 11:14)
- Mutual recursion with Equations (8 messages, latest: Aug 27 2024 at 11:33)
- Generated induction principle is unhelpful (10 messages, latest: Aug 26 2024 at 17:13)
- Inlining Inspect when using a with ? (3 messages, latest: Aug 19 2024 at 13:08)
- Equations "with" syntax (3 messages, latest: Aug 02 2024 at 10:42)
- Equations: Common arguments (6 messages, latest: Aug 02 2024 at 08:19)
- Lacking information when using wf + with (18 messages, latest: Jul 12 2024 at 09:06)
- Equations tag for 8.20 (10 messages, latest: Jul 10 2024 at 10:37)
- Equations fails with coinductive types? (1 message, latest: Jun 24 2024 at 12:50)
- Help needed: tutorial Equations and well-founded rec (2 messages, latest: Jun 12 2024 at 13:37)
- Bug funelim on Ack (39 messages, latest: May 29 2024 at 10:16)
- Tutorials for Equations (5 messages, latest: May 21 2024 at 16:47)
- Equations vs Equations? (3 messages, latest: May 17 2024 at 15:47)
- Suppress warnings? (9 messages, latest: Jan 26 2024 at 09:41)
- Solving equations obligations (9 messages, latest: Jan 09 2024 at 15:14)
- Opam package failing on 8.18? (12 messages, latest: Jan 04 2024 at 14:58)
- Induction principle (13 messages, latest: Dec 22 2023 at 15:02)
- 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: Oct 08 2024 at 14:01 UTC