Topics:
- Coq documentation (9 messages, latest: Mar 20 2023 at 10:26)
- Lambda clam (25 messages, latest: Mar 19 2023 at 19:46)
- Interaction between ocaml and coq-ELPI (1 message, latest: Mar 14 2023 at 10:43)
- Prolog extension for Monte Carlo Proof Search (4 messages, latest: Mar 09 2023 at 12:44)
- Flexible term outside pattern fragment (2 messages, latest: Mar 08 2023 at 20:44)
- Code behaving differently in commands and tactics (4 messages, latest: Mar 02 2023 at 10:24)
- Difference between var and uvar (4 messages, latest: Feb 27 2023 at 21:03)
- Adding a clause with a body to the context (4 messages, latest: Feb 27 2023 at 11:10)
- Association list of variables encoded in CHR + same_var (14 messages, latest: Feb 22 2023 at 13:52)
- Hide std.map type (3 messages, latest: Feb 07 2023 at 15:34)
- opam install coq-elpi (7 messages, latest: Jan 30 2023 at 22:21)
- app constructor (1 message, latest: Jan 27 2023 at 08:38)
- Generating proof terms containing Ltac (6 messages, latest: Jan 23 2023 at 09:33)
- Compilation of coq-elpi on Coq master (6 messages, latest: Jan 18 2023 at 19:35)
- Elpi Deriving (15 messages, latest: Jan 17 2023 at 17:18)
- ✔ Non closed Term (12 messages, latest: Dec 21 2022 at 15:38)
- ✔ Reducing integers (4 messages, latest: Dec 20 2022 at 20:44)
- Why did Elpi ended up looking like Elpi (5 messages, latest: Dec 11 2022 at 00:01)
- `.glob` entries from elpi (7 messages, latest: Dec 01 2022 at 11:05)
- Derive the name of the enclosing file level module (9 messages, latest: Nov 24 2022 at 14:57)
- Local version of coq.locate (2 messages, latest: Nov 19 2022 at 20:23)
- Preprocessing before itauto (7 messages, latest: Nov 15 2022 at 10:42)
- ✔ Using Query on a Db (4 messages, latest: Nov 11 2022 at 16:29)
- ✔ When does coq.elpi.accumulate take effect? (4 messages, latest: Nov 10 2022 at 15:48)
- coq.elaborate-skeleton generates fresh universes (12 messages, latest: Nov 10 2022 at 15:24)
- Typo in new Coq-Elpi tag (2 messages, latest: Nov 10 2022 at 13:58)
- ✔ Coq Platform CI failure (28 messages, latest: Nov 03 2022 at 18:18)
- Quotation for `constructor` (17 messages, latest: Oct 28 2022 at 08:51)
- Non-deterministic pruning (6 messages, latest: Oct 27 2022 at 08:57)
- How inspect terms under binders in Elpi (11 messages, latest: Oct 26 2022 at 13:18)
- ✔ Question on tutorial (4 messages, latest: Oct 26 2022 at 09:52)
- unknown inductive error on match (5 messages, latest: Oct 25 2022 at 09:34)
- use of copy with variables (17 messages, latest: Oct 24 2022 at 13:10)
- ELPI plugin for VSCodium (11 messages, latest: Oct 17 2022 at 15:03)
- Collecting constructor arguments (13 messages, latest: Oct 12 2022 at 12:59)
- LGPL license of examples and `apps` in coq-elpi (7 messages, latest: Oct 12 2022 at 08:27)
- Performance of wrapping `decide equality` (6 messages, latest: Oct 12 2022 at 00:43)
- Error "Not Yet Implemented: HOAS SFBmind" with Module API (31 messages, latest: Oct 11 2022 at 16:03)
- Possible bug related to implicit arguments (7 messages, latest: Oct 07 2022 at 21:00)
- Error `Not a variable after goal` (4 messages, latest: Oct 04 2022 at 14:19)
- fix constructor argument (3 messages, latest: Sep 26 2022 at 13:36)
- Recursive Elpi tactic, or predicate modifying the goal (15 messages, latest: Sep 23 2022 at 14:09)
- ✔ [beginner] Arguments of a tactic defined with `Elpi` (5 messages, latest: Sep 19 2022 at 19:09)
- Reifying terms with ltac / if-then-else / complex match (19 messages, latest: Sep 15 2022 at 16:29)
- ✔ Elpi tactic returning a term (7 messages, latest: Sep 14 2022 at 10:38)
- ✔ Outputting a list of variables (13 messages, latest: Sep 14 2022 at 10:38)
- ✔ Problem of unifying evars? (6 messages, latest: Sep 14 2022 at 10:38)
- Error "Unification problem outside the pattern fragment." (6 messages, latest: Sep 07 2022 at 14:11)
- Accumulate to a database during execution (3 messages, latest: Sep 01 2022 at 14:12)
- Running issues (5 messages, latest: Aug 18 2022 at 12:31)
- Issues with latest Elpi on Windows (11 messages, latest: Aug 13 2022 at 19:51)
- Proof obligations (4 messages, latest: Aug 12 2022 at 20:31)
- all_different constraint (5 messages, latest: Aug 03 2022 at 08:31)
- elpi -> ltac1 -> vm_compute = normal cast (22 messages, latest: Jul 23 2022 at 17:58)
- Calling external tools with Coq-Elpi (12 messages, latest: Jul 22 2022 at 20:47)
- Using `abstract` from Ltac1 in Elpi (10 messages, latest: Jul 22 2022 at 20:09)
- Recursive Predicate (4 messages, latest: Jul 20 2022 at 13:00)
- State Injectivity (19 messages, latest: Jul 20 2022 at 09:53)
- Question on error message "Evaluation of a non closed term" (8 messages, latest: Jul 20 2022 at 07:16)
- ✔ !tactic_mode (9 messages, latest: Jul 16 2022 at 20:36)
- ✔ Adding universe polymorphic inductive type (8 messages, latest: Jul 16 2022 at 20:36)
- `idtac` and then `clearbody`on a list (of lists) of terms (9 messages, latest: Jul 08 2022 at 08:37)
- Unifying a sort with Set (6 messages, latest: Jul 06 2022 at 17:08)
- Unification variable under binders (2 messages, latest: May 19 2022 at 20:02)
- coq-elpi on `coq.dev` again (23 messages, latest: May 15 2022 at 23:40)
- ✔ Spilling under a binder (14 messages, latest: May 11 2022 at 08:42)
- Macro tutorial (2 messages, latest: May 09 2022 at 15:25)
- Removing a clause from an Elpi database (6 messages, latest: May 09 2022 at 13:50)
- ✔ coq-elpi broken on `coq.dev`? (5 messages, latest: May 05 2022 at 17:27)
- Universe polymorphism (9 messages, latest: May 05 2022 at 07:16)
- Elpi applications besides HB (8 messages, latest: May 04 2022 at 08:41)
- Making this stream web-public (2 messages, latest: Apr 19 2022 at 08:30)
- stream events (2 messages, latest: Apr 16 2022 at 16:54)
- First experience report (5 messages, latest: Apr 15 2022 at 17:38)
- [Beginner question] about binding with `pi`and `decl` (3 messages, latest: Apr 13 2022 at 13:41)
- Definition of copy (2 messages, latest: Apr 11 2022 at 18:11)
- Question on occurs (11 messages, latest: Apr 07 2022 at 14:36)
- What is the syntax of comments? (3 messages, latest: Apr 05 2022 at 06:39)
- New elpi variables when asserting a new goal (7 messages, latest: Apr 04 2022 at 11:59)
- Elpi version for Coq Platform (3 messages, latest: Mar 21 2022 at 10:57)
- `Elpi Debug` (5 messages, latest: Mar 16 2022 at 09:13)
- mlock Implicits (19 messages, latest: Feb 28 2022 at 14:59)
- Find a hypothesis in a sealed-goal (4 messages, latest: Feb 25 2022 at 19:35)
- RawData data model (5 messages, latest: Feb 23 2022 at 10:47)
- Elpi as a Type Classes resolution engine (28 messages, latest: Feb 22 2022 at 16:48)
- Elpi API (2 messages, latest: Feb 18 2022 at 13:03)
- Support for fixpoints (12 messages, latest: Feb 17 2022 at 17:34)
- ✔ citation (4 messages, latest: Feb 14 2022 at 08:49)
- coq-elpi fails to build on mathcom-dev:coq-dev docker image (4 messages, latest: Feb 10 2022 at 09:16)
- elpi and coqdep (80 messages, latest: Feb 03 2022 at 13:51)
- `Elpi Accumulate File` and Coq's `LoadPath` (35 messages, latest: Feb 03 2022 at 13:07)
- Hint Resolve (7 messages, latest: Feb 01 2022 at 21:51)
- ✔ Generating terms via ltac in an [Elpi Command] (16 messages, latest: Jan 26 2022 at 21:55)
- Functors (6 messages, latest: Jan 25 2022 at 21:21)
- Functors Implementation tradeoff (4 messages, latest: Jan 25 2022 at 18:08)
- Parens / command parsing (5 messages, latest: Jan 20 2022 at 21:20)
- Hint Opaque (6 messages, latest: Jan 20 2022 at 20:27)
- Revert on section variable "forgotten" by an elpi tactic (2 messages, latest: Dec 09 2021 at 16:18)
- Opaque bodies (5 messages, latest: Dec 03 2021 at 06:21)
- Local context update (2 messages, latest: Nov 18 2021 at 14:33)
- Using Conversion in Elpi's OCaml API (4 messages, latest: Nov 08 2021 at 09:51)
- Updated tutorials (7 messages, latest: Sep 28 2021 at 14:38)
- Create new goal (assert in Elpi) (6 messages, latest: Sep 01 2021 at 17:55)
- Pure tactic (7 messages, latest: Aug 20 2021 at 08:50)
- Tactic populating database at runtime does not work (12 messages, latest: Jul 22 2021 at 12:36)
- Abstract over "derive" (2 messages, latest: Jul 16 2021 at 05:41)
- Use case of induction over rose trees (2 messages, latest: Jul 13 2021 at 16:30)
- Print context (8 messages, latest: Jul 07 2021 at 09:48)
- Duplicate context entry (5 messages, latest: Jul 02 2021 at 12:45)
- Unification variable depending on term (31 messages, latest: Jul 02 2021 at 10:06)
- No notion of scope (10 messages, latest: Jun 29 2021 at 17:02)
- ease of debugging (5 messages, latest: Jun 03 2021 at 16:38)
- Elpi does not find database (6 messages, latest: Jun 02 2021 at 14:23)
- cut type error (3 messages, latest: Jun 01 2021 at 14:47)
- Inlining files containing `Elpi Accumulate File` (6 messages, latest: May 25 2021 at 07:33)
- Record Import (6 messages, latest: Apr 30 2021 at 06:29)
- Using Elpi with Emacs/PG (6 messages, latest: Apr 30 2021 at 06:09)
- coq-elpi.dev fails to build against coq.dev (16 messages, latest: Apr 25 2021 at 07:55)
- Predicate to associate Elpi `int` and Coq terms of `N` (7 messages, latest: Apr 22 2021 at 08:31)
- Abstract function application (5 messages, latest: Apr 15 2021 at 10:32)
- Generating large Coq term of type `list N` in Elpi (17 messages, latest: Apr 10 2021 at 16:38)
- Forcing garbage collection (2 messages, latest: Apr 10 2021 at 11:30)
- Set merge does not remove duplicates (3 messages, latest: Mar 04 2021 at 16:35)
- Synthesizing an Elpi clause from a Coq term with holes (6 messages, latest: Feb 28 2021 at 17:30)
- matching with function application (5 messages, latest: Feb 22 2021 at 11:37)
- new proof context variables or definitions (17 messages, latest: Feb 19 2021 at 07:17)
- Rewrite in Coq-Elpi (3 messages, latest: Feb 18 2021 at 20:04)
- Goal manipulation (3 messages, latest: Feb 18 2021 at 05:39)
- Map with Coq terms as keys (3 messages, latest: Feb 11 2021 at 16:47)
- Renaming a subterm (8 messages, latest: Feb 09 2021 at 11:16)
- Creating a Coq function in Coq-Elpi (7 messages, latest: Feb 08 2021 at 14:42)
- Custom reduction (14 messages, latest: Jan 25 2021 at 19:16)
- Typing in coq-elpi (4 messages, latest: Jan 25 2021 at 17:03)
- Elpi goal rewriting (4 messages, latest: Dec 01 2020 at 14:39)
- coq-elpi fails to build on coqorg/coq:dev docker image (12 messages, latest: Nov 30 2020 at 15:51)
- Support for mutually inductive types (8 messages, latest: Nov 25 2020 at 14:10)
- inductive predicate to boolean function (9 messages, latest: Nov 14 2020 at 13:15)
- Elpi on Windows (21 messages, latest: Sep 16 2020 at 13:50)
- Tactician (21 messages, latest: Sep 12 2020 at 17:25)
- Examples (2 messages, latest: Aug 30 2020 at 06:28)
Last updated: Mar 25 2023 at 07:28 UTC