Stream: MetaCoq

Topics:

• Bugs (3 messages, latest: Oct 08 2024 at 13:33)
• Reasoning about generated MetaCoq code (61 messages, latest: Oct 03 2024 at 09:31)
• Unquoting inductive type (2 messages, latest: Sep 19 2024 at 01:17)
• ✔ Mistake noccur_between ? (3 messages, latest: Sep 17 2024 at 20:28)
• ✔ Name vs option ident (1 message, latest: Sep 17 2024 at 15:10)
• ✔ Computing free variables (2 messages, latest: Sep 17 2024 at 15:10)
• Computing free variables (4 messages, latest: Sep 16 2024 at 18:01)
• How to hnf a template term with metacoq (18 messages, latest: Sep 14 2024 at 10:50)
• Citing metacoq (5 messages, latest: Sep 12 2024 at 10:48)
• Name vs option ident (12 messages, latest: Sep 09 2024 at 13:08)
• ✔ Releases (2 messages, latest: Sep 03 2024 at 12:03)
• Releases (1 message, latest: Sep 03 2024 at 10:46)
• Docker images for CI (5 messages, latest: Aug 21 2024 at 12:14)
• Well-Typedness for Inductives (5 messages, latest: Jul 27 2024 at 11:05)
• ✔ coq-metacoq-template 1.2.1+8.18 suddenly failing in CI (8 messages, latest: Jul 24 2024 at 07:36)
• coq-metacoq-template 1.2.1+8.18 suddenly failing in CI (64 messages, latest: Jul 23 2024 at 15:49)
• Status of verified extraction (42 messages, latest: Jul 23 2024 at 07:34)
• ✔ Unbearably slow compilation of some Coq files (3 messages, latest: Jun 05 2024 at 16:24)
• Unbearably slow compilation of some Coq files (3 messages, latest: Jun 05 2024 at 13:52)
• tmUnquote and printing a term in SProp (9 messages, latest: May 28 2024 at 20:27)
• tmPrint in a file ? (8 messages, latest: May 22 2024 at 19:05)
• Notation tProd Anon ? (7 messages, latest: May 13 2024 at 08:53)
• Basics of MetaCoq - How to inline quote/unquote (3 messages, latest: May 01 2024 at 07:56)
• Lean meta programming (3 messages, latest: Apr 01 2024 at 15:06)
• Constructor and backtracking (7 messages, latest: Mar 31 2024 at 12:48)
• Formalizing inductive families. (20 messages, latest: Mar 01 2024 at 16:54)
• MetaCoq Tutorial at POPL (144 messages, latest: Feb 19 2024 at 16:54)
• ✔ Get modpath of file (1 message, latest: Feb 15 2024 at 13:10)
• Get modpath of file (2 messages, latest: Feb 15 2024 at 09:37)
• Example plugins with metacoq (4 messages, latest: Feb 11 2024 at 05:25)
• Cbn vs simpl in MetaCoq (34 messages, latest: Feb 06 2024 at 14:40)
• Metacoq notations (41 messages, latest: Jan 31 2024 at 21:33)
• Necessary fields for tmMkInductive' (3 messages, latest: Jan 25 2024 at 09:46)
• Boolean equality on template terms (6 messages, latest: Dec 15 2023 at 13:17)
• make all and translations (2 messages, latest: Dec 13 2023 at 12:57)
• MetaCoq on 32-bit OCaml (7 messages, latest: Dec 13 2023 at 12:57)
• documentation for the quotation package? (2 messages, latest: Dec 13 2023 at 12:56)
• Adding constraints to Record based on Parameters and Fields (1 message, latest: Nov 30 2023 at 19:10)
• Updating the default branch (1 message, latest: Nov 28 2023 at 19:34)
• Equivalence of single-constructor inductives with definition (12 messages, latest: Nov 02 2023 at 12:58)
• Splicing a kername (19 messages, latest: Oct 27 2023 at 11:19)
• Release tag for a version working with Coq 8.18 (4 messages, latest: Oct 26 2023 at 07:58)
• Using notations for pretty printing terms (6 messages, latest: Oct 26 2023 at 07:46)
• stdlib-shims and compilation in _build_ci (6 messages, latest: Oct 20 2023 at 09:24)
• MetaCoq Quotation Slide Deck (4 messages, latest: Oct 18 2023 at 06:18)
• coq-native (1 message, latest: Oct 18 2023 at 02:25)
• Release tag for 1.3+8.18 (9 messages, latest: Oct 16 2023 at 07:34)
• default branch (2 messages, latest: Sep 30 2023 at 15:26)
• Theorems about inductive type descriptions (11 messages, latest: Sep 13 2023 at 16:19)
• MetaCoq for AST generation (27 messages, latest: Aug 17 2023 at 07:11)
• Constructing Records and Classes (11 messages, latest: Jul 13 2023 at 17:03)
• Call for help: Rosetta stone for Metaprogramming in Coq (5 messages, latest: Jun 28 2023 at 18:28)
• Magmide (8 messages, latest: Jun 24 2023 at 14:23)
• Merge Policy (1 message, latest: Jun 19 2023 at 14:12)
• PR Review? (45 messages, latest: Jun 03 2023 at 23:50)
• erasurefunction taking lots of memory? (5 messages, latest: May 27 2023 at 16:08)
• Performance Info (12 messages, latest: May 22 2023 at 11:07)
• Soundness vs Strong Normalization (14 messages, latest: May 16 2023 at 09:00)
• SafeChecker invocation? (14 messages, latest: Apr 26 2023 at 09:01)
• Universes of term? (5 messages, latest: Apr 26 2023 at 07:12)
• Monad utils / new ExtLib dependency (3 messages, latest: Apr 25 2023 at 07:32)
• 8.17 version / Coq Platform 2022.03 beta (24 messages, latest: Apr 24 2023 at 19:20)
• SafeChecker on open terms? (16 messages, latest: Apr 19 2023 at 20:36)
• Non-squashed typing judgments (58 messages, latest: Apr 18 2023 at 15:02)
• `type_mkApps` (2 messages, latest: Apr 17 2023 at 07:26)
• ✔ generalizing from typing in the empty context (4 messages, latest: Apr 14 2023 at 22:36)
• generalizing from typing in the empty context (6 messages, latest: Apr 14 2023 at 21:58)
• sync 8.16 and master branches (2 messages, latest: Apr 13 2023 at 10:16)
• PCUIC Quotation (1 message, latest: Apr 13 2023 at 08:05)
• understanding inductive types (40 messages, latest: Apr 11 2023 at 11:27)
• ✔ maste (1 message, latest: Apr 11 2023 at 06:12)
• maste (3 messages, latest: Apr 05 2023 at 06:22)
• Gallina quotation (2 messages, latest: Apr 05 2023 at 01:30)
• Fixing dynlink errors? (3 messages, latest: Apr 03 2023 at 10:12)
• Nix CI broken? (22 messages, latest: Apr 03 2023 at 06:40)
• Options in `tm_util` (8 messages, latest: Mar 30 2023 at 08:15)
• tmTry (5 messages, latest: Mar 26 2023 at 20:47)
• CI failure (52 messages, latest: Mar 23 2023 at 13:28)
• ✔ Error when stepping the code from erasure_live_test.v (16 messages, latest: Mar 06 2023 at 10:44)
• Frustrating universe errors? (6 messages, latest: Feb 28 2023 at 05:14)
• tmExistingInstance (3 messages, latest: Feb 28 2023 at 04:40)
• segfaults? (3 messages, latest: Feb 28 2023 at 04:39)
• compilation errors not in the wiki (3 messages, latest: Feb 24 2023 at 15:52)
• TemplateMonad and SProp? (1 message, latest: Feb 21 2023 at 23:25)
• tmQuoteModule deficiencies (2 messages, latest: Feb 21 2023 at 20:44)
• mkLambda / closing a locally nameless term (3 messages, latest: Feb 14 2023 at 21:28)
• universe constraints in template monad programs (1 message, latest: Feb 14 2023 at 02:55)
• global_reference -> term in the template monad (1 message, latest: Feb 14 2023 at 02:35)
• Template and PCUIC (4 messages, latest: Feb 13 2023 at 13:59)
• Gallina quotation functions (9 messages, latest: Feb 12 2023 at 03:25)
• Build errors (coq#17022) (2 messages, latest: Feb 08 2023 at 15:50)
• Build errors (coq#17021) (7 messages, latest: Jan 17 2023 at 14:58)
• running TemplateMonad inside a tactic (6 messages, latest: Jan 14 2023 at 12:43)
• plugins in MetaCoq vs. ML (4 messages, latest: Dec 27 2022 at 11:11)
• Build errors (12 messages, latest: Dec 15 2022 at 10:52)
• Global environment extension modulo ordering (15 messages, latest: Dec 14 2022 at 16:29)
• Why `extends_decls` in `PCUICElimination.Informative` (2 messages, latest: Dec 13 2022 at 11:56)
• Doing better than a Trusted Theory Base (55 messages, latest: Dec 09 2022 at 22:58)
• uGraph.consistent_ext_on_full_ext (14 messages, latest: Dec 09 2022 at 12:38)
• Translation to W types? (8 messages, latest: Dec 09 2022 at 11:01)
• Merging PRs (3 messages, latest: Dec 08 2022 at 09:31)
• ✔ `cored` and `extends_decls` (19 messages, latest: Dec 08 2022 at 09:29)
• Changing global universes in typing (7 messages, latest: Dec 07 2022 at 22:39)
• Stack overflow during a tactic (4 messages, latest: Dec 07 2022 at 16:21)
• Template Monad universes (1 message, latest: Nov 28 2022 at 19:26)
• extends (2 messages, latest: Nov 27 2022 at 20:16)
• template-coq/gen-src/cRelationClasses.mli.orig (1 message, latest: Nov 25 2022 at 00:44)
• Axioms vs (typeclass) hypotheses (9 messages, latest: Nov 25 2022 at 00:44)
• Set Suggest Proof Using (17 messages, latest: Nov 24 2022 at 20:33)
• Proving typing of `<% ... %>` (19 messages, latest: Nov 24 2022 at 18:58)
• Prop (12 messages, latest: Nov 24 2022 at 11:33)
• inspect on recursive calls (7 messages, latest: Nov 24 2022 at 11:31)
• Lack of decidable equality (32 messages, latest: Nov 24 2022 at 11:29)
• adding False to Σ (1 message, latest: Nov 24 2022 at 00:07)
• ✔ ConstraintSet.t -> LevelSet.t (3 messages, latest: Nov 23 2022 at 13:52)
• ✔ quoting `valid_constraints` for quoting typing judgments (40 messages, latest: Nov 23 2022 at 13:51)
• ✔ Checking universe graph? (5 messages, latest: Nov 23 2022 at 13:50)
• Non-squashed typing judgments? (3 messages, latest: Nov 23 2022 at 13:40)
• tmUnquote (4 messages, latest: Nov 23 2022 at 13:38)
• ✔ guard checker (5 messages, latest: Nov 23 2022 at 13:10)
• Debugging anomalies (2 messages, latest: Nov 23 2022 at 12:38)
• Free variables? (8 messages, latest: Nov 23 2022 at 12:34)
• Working with PCUICAst (8 messages, latest: Nov 23 2022 at 12:22)
• `tmFix`point combinator (39 messages, latest: Nov 22 2022 at 00:10)
• Fueling the checker (20 messages, latest: Nov 11 2022 at 20:07)
• ✔ `on_ind_body` (6 messages, latest: Nov 07 2022 at 23:10)
• ✔ Build errors (17 messages, latest: Nov 07 2022 at 23:10)
• ✔ Template.TypingWf.on_option (5 messages, latest: Nov 07 2022 at 23:08)
• ✔ Typing.v Prop vs bool (4 messages, latest: Nov 07 2022 at 23:08)
• squashing in infer_template_program? (2 messages, latest: Nov 04 2022 at 06:30)
• Determining when a constant is global? (9 messages, latest: Oct 31 2022 at 17:29)
• mutual_inductive_entry (7 messages, latest: Oct 26 2022 at 13:42)
• Async fails to load MetaCoq (6 messages, latest: Oct 25 2022 at 17:42)
• ✔ Implicits intros in tmLemma (14 messages, latest: Oct 24 2022 at 11:16)
• properties of MetaCoq/PCUIC (32 messages, latest: Oct 22 2022 at 21:00)
• Tactics in MetaCoq (26 messages, latest: Oct 13 2022 at 08:55)
• ✔ Why is wf_local is not mutual recursion with `typing` (33 messages, latest: Oct 10 2022 at 13:41)
• Use of tmLemma (6 messages, latest: Oct 05 2022 at 21:12)
• MetaCoq 1.0 problems for 8.16 (49 messages, latest: Sep 22 2022 at 13:03)
• Reification of operations on Z (12 messages, latest: Aug 31 2022 at 15:41)
• CI (31 messages, latest: Aug 05 2022 at 10:38)
• Access the defined constant of tmMkInductive (8 messages, latest: Jul 06 2022 at 09:37)
• Typeclasses (4 messages, latest: Jun 28 2022 at 12:35)
• StackExchange on guard condition stuff (2 messages, latest: May 25 2022 at 12:15)
• Universes for new inductive (22 messages, latest: May 06 2022 at 17:30)
• stream events (2 messages, latest: May 04 2022 at 07:51)
• opam install metacoq-template does not work on MacOs (58 messages, latest: Apr 26 2022 at 13:22)
• REPL for MetaCoq? (61 messages, latest: Feb 15 2022 at 13:10)
• ✔ TemplateMonad: get constructors of inductive type (21 messages, latest: Jan 07 2022 at 10:00)
• Significance of template-coq record fields (23 messages, latest: Jan 07 2022 at 08:03)
• Way to call unquote from a coq function (11 messages, latest: Jan 07 2022 at 05:43)
• Descriptions of fields of record types in template-coq (4 messages, latest: Jan 03 2022 at 07:23)
• ✔ Definition of kername (7 messages, latest: Dec 30 2021 at 17:00)
• ✔ Error on trying add_constructor example (9 messages, latest: Dec 30 2021 at 10:36)
• The META file (3 messages, latest: Nov 30 2021 at 14:05)
• Infer implicit types during unquoting (24 messages, latest: Nov 12 2021 at 10:23)
• build failure on case insensitive filesystem (1 message, latest: Nov 08 2021 at 16:57)
• Certified OCaml extraction (8 messages, latest: Oct 13 2021 at 18:37)
• migrate metacoq to coq-hott (3 messages, latest: Oct 06 2021 at 20:50)
• How to speed up Metacoq compile time (35 messages, latest: Sep 02 2021 at 14:16)
• Strange Error when Compile PCUICWcbvEval.v (4 messages, latest: Aug 28 2021 at 07:41)
• Why the erasure target language is untyped? (6 messages, latest: Aug 23 2021 at 09:22)
• ✔ Notation clash with Int63 (13 messages, latest: Jul 12 2021 at 09:55)
• Some low-level questions about consistent (7 messages, latest: Jul 12 2021 at 08:51)
• opam install not working (59 messages, latest: Jun 25 2021 at 16:03)
• No rule to make target tm_util.cmx (16 messages, latest: Jun 06 2021 at 16:23)
• question about impredicative set (10 messages, latest: May 04 2021 at 06:52)
• Recursive Quote Tactic (3 messages, latest: Mar 04 2021 at 10:50)
• error from opam (24 messages, latest: Feb 16 2021 at 19:10)
• Make MetaCoq Run use a different reduction strategy (9 messages, latest: Dec 16 2020 at 19:34)
• Adding new types to the quoting mechanism (4 messages, latest: Dec 10 2020 at 13:21)
• Efficient substitutions For Reals (3 messages, latest: Dec 08 2020 at 18:19)
• Primitive types in MetaCoq (16 messages, latest: Dec 08 2020 at 13:04)
• Which meta-language to choose? (11 messages, latest: Dec 03 2020 at 16:10)
• Adding a un/quoted term (or its type) in the environment (11 messages, latest: Nov 30 2020 at 15:44)
• Failure in Coq's CI (7 messages, latest: Nov 19 2020 at 13:22)
• wf_universes and reduction (2 messages, latest: Nov 18 2020 at 11:59)
• MetaCoq depends on time command? (25 messages, latest: Oct 05 2020 at 13:28)
• MetaCoq CI / Coq Community CI (19 messages, latest: Oct 01 2020 at 17:25)
• Proving a reified proposition with Program (10 messages, latest: Sep 30 2020 at 08:01)
• errors in coq CI log (2 messages, latest: Sep 24 2020 at 14:34)
• Moving erased eval to Type (5 messages, latest: Sep 23 2020 at 13:00)
• de Bruijn indices while declaring inductive (5 messages, latest: Sep 22 2020 at 13:03)
• News (2 messages, latest: Sep 15 2020 at 19:46)
• red_proj, eval_proj and multi-constructor inductives (6 messages, latest: Sep 15 2020 at 19:23)
• Discarding tEvar (5 messages, latest: Sep 08 2020 at 13:55)
• OPAM version ordering fixes (11 messages, latest: Sep 07 2020 at 09:43)
• Quoting the current global environment (4 messages, latest: Sep 04 2020 at 12:25)
• Are typing derivations property ? (13 messages, latest: Aug 28 2020 at 09:15)
• Difference between existential variables and metavariables (4 messages, latest: Jul 31 2020 at 13:02)
• Trying out metacoq (41 messages, latest: Jul 28 2020 at 16:39)
• Erasure evaluation relation is nondeterministic (41 messages, latest: Jul 20 2020 at 09:30)
• New local assumption / weakening (8 messages, latest: Jul 06 2020 at 07:36)
• Parametericity translation (4 messages, latest: Jul 05 2020 at 14:31)
• Flag for typing judgments (4 messages, latest: Jul 03 2020 at 15:28)
• Mismatch about printed name of a constructor (4 messages, latest: Jun 30 2020 at 09:33)
• Compatibility with Equations 1.2.2 (4 messages, latest: Jun 26 2020 at 08:49)
• Dis/proving a meta-theoretical question (33 messages, latest: Jun 19 2020 at 15:07)
• Unquote and quote does work using Prop (14 messages, latest: Jun 12 2020 at 14:51)
• Shape of case branches (9 messages, latest: Jun 11 2020 at 09:07)
• tmUnquoteTyped (5 messages, latest: Jun 10 2020 at 08:43)
• hnf/reduce_term (22 messages, latest: Jun 04 2020 at 09:56)
• imported from gitter room coq/metacoq (346 messages, latest: May 06 2020 at 01:59)

Last updated: Oct 12 2024 at 11:01 UTC