Stream: Coq users

Topics:

• New Stack Exchange question (1063 messages, latest: May 30 2023 at 21:44)
• existing elements (1 message, latest: May 26 2023 at 10:02)
• Commands Fail and Succeed (2 messages, latest: May 25 2023 at 07:23)
• use of bool symtry (6 messages, latest: May 22 2023 at 15:22)
• ✔ Simple question about removing duplicates from a list (25 messages, latest: May 20 2023 at 11:47)
• Denotational semantics without excluded middle (13 messages, latest: May 17 2023 at 22:49)
• How to simplify ? (10 messages, latest: May 17 2023 at 16:44)
• ✔ Implicit coercions for length-indexed list (2 messages, latest: May 16 2023 at 18:50)
• Implicit coercions for length-indexed list (11 messages, latest: May 16 2023 at 17:50)
• Why not binary nats ? (20 messages, latest: May 16 2023 at 09:32)
• Padding bitvectors (8 messages, latest: May 16 2023 at 08:49)
• Avoiding infinite loop (4 messages, latest: May 15 2023 at 17:44)
• argument (2 messages, latest: May 14 2023 at 11:50)
• same output (2 messages, latest: May 14 2023 at 09:12)
• Destructing dependent matches (3 messages, latest: May 13 2023 at 11:28)
• New Discourse topics (232 messages, latest: May 11 2023 at 19:52)
• ✔ Global Hint Extern (4 messages, latest: May 11 2023 at 16:55)
• ✔ Typeclasses and Print (2 messages, latest: May 11 2023 at 15:11)
• Typeclasses and Print (2 messages, latest: May 11 2023 at 14:33)
• list of points (98 messages, latest: May 11 2023 at 12:43)
• Simple properties of natural numbers (3 messages, latest: May 10 2023 at 06:36)
• Noisy printing with name mangling light (21 messages, latest: May 09 2023 at 18:28)
• (Lack of) Coq renaming (10 messages, latest: May 08 2023 at 23:17)
• full_fill condition (1 message, latest: May 06 2023 at 06:14)
• empty list case (21 messages, latest: May 04 2023 at 07:04)
• notation confusion (6 messages, latest: May 02 2023 at 21:47)
• hypothesis (4 messages, latest: May 02 2023 at 14:04)
• WebAssembly (3 messages, latest: May 01 2023 at 16:11)
• use of same command (3 messages, latest: May 01 2023 at 15:13)
• meaning of following command (2 messages, latest: May 01 2023 at 07:43)
• Various uses of turnstile symbol in the following code (4 messages, latest: Apr 30 2023 at 20:11)
• Trivial goal with minus operation (7 messages, latest: Apr 30 2023 at 05:31)
• selection of variable (5 messages, latest: Apr 30 2023 at 05:09)
• e-graphs in Coq? (6 messages, latest: Apr 29 2023 at 21:28)
• conversion of data type (19 messages, latest: Apr 29 2023 at 06:50)
• Error message says a type is incompatible with itself. (4 messages, latest: Apr 29 2023 at 02:03)
• Backwards compatibility w.r.t. Div0 without warnings (21 messages, latest: Apr 28 2023 at 15:30)
• Keyed Unification (10 messages, latest: Apr 28 2023 at 13:14)
• understanding strict/nested Positivity (19 messages, latest: Apr 28 2023 at 11:27)
• Handling many equivalent statements with automation (1 message, latest: Apr 27 2023 at 23:17)
• cbn in primitive projections (14 messages, latest: Apr 27 2023 at 13:52)
• trusted code base (19 messages, latest: Apr 27 2023 at 07:44)
• repo for testing positivity check implementation (2 messages, latest: Apr 26 2023 at 16:08)
• ✔ Proving forall (n m: nat), n = m + (n - m). (2 messages, latest: Apr 26 2023 at 13:50)
• How to replace one notation with another project-wide (4 messages, latest: Apr 26 2023 at 08:24)
• Proving forall (n m: nat), n = m + (n - m). (6 messages, latest: Apr 25 2023 at 15:58)
• Knights and Knaves puzzle (4 messages, latest: Apr 24 2023 at 21:32)
• Ideas on how to create custom list map (6 messages, latest: Apr 24 2023 at 18:23)
• Inversion on Sets (14 messages, latest: Apr 24 2023 at 16:49)
• Using hypotheses in automation (6 messages, latest: Apr 24 2023 at 16:00)
• Multi-statement abstract (12 messages, latest: Apr 24 2023 at 09:40)
• ✔ Not an arity for Inductive Type (2 messages, latest: Apr 23 2023 at 20:32)
• Not an arity for Inductive Type (3 messages, latest: Apr 23 2023 at 06:53)
• "Reset Initial" memory impacts (3 messages, latest: Apr 23 2023 at 00:40)
• Dependent types and equality (6 messages, latest: Apr 22 2023 at 18:54)
• Ltac on shelved goals (10 messages, latest: Apr 21 2023 at 19:29)
• dependent sum subtypes (2 messages, latest: Apr 20 2023 at 19:29)
• ✔ Proof without suitable constructor (3 messages, latest: Apr 20 2023 at 03:27)
• ✔ type inference in `let in` expression (3 messages, latest: Apr 20 2023 at 02:13)
• Super-slow/diverging `simpl` without debug output (23 messages, latest: Apr 19 2023 at 21:07)
• Proof without suitable constructor (2 messages, latest: Apr 19 2023 at 17:16)
• type inference in `let in` expression (2 messages, latest: Apr 19 2023 at 08:25)
• ✔ Changing default names when using induction (2 messages, latest: Apr 19 2023 at 07:25)
• list & its members (8 messages, latest: Apr 19 2023 at 05:51)
• Code review / simplifying repetition (7 messages, latest: Apr 18 2023 at 23:05)
• Changing default names when using induction (3 messages, latest: Apr 18 2023 at 15:51)
• ✔ Case Analysis with Dependent Records (4 messages, latest: Apr 17 2023 at 15:59)
• How to use debug flag? (7 messages, latest: Apr 17 2023 at 15:42)
• efficient way (29 messages, latest: Apr 17 2023 at 12:55)
• Case Analysis with Dependent Records (14 messages, latest: Apr 17 2023 at 11:24)
• use of lia. (13 messages, latest: Apr 17 2023 at 09:25)
• Clearing trivial hypotheses (9 messages, latest: Apr 17 2023 at 00:00)
• opaque function that I didn't set (8 messages, latest: Apr 16 2023 at 18:52)
• ✔ Coqhammer (9 messages, latest: Apr 16 2023 at 18:04)
• Use of In (3 messages, latest: Apr 16 2023 at 08:54)
• add conditions (2 messages, latest: Apr 15 2023 at 12:37)
• Library (4 messages, latest: Apr 15 2023 at 11:54)
• Change in occs_nums syntax (6 messages, latest: Apr 15 2023 at 07:37)
• conflict in statements (13 messages, latest: Apr 15 2023 at 06:02)
• How is coq implemented? (6 messages, latest: Apr 14 2023 at 16:50)
• co-existence (7 messages, latest: Apr 14 2023 at 06:45)
• ✔ Simple things I can't get coq-interval to solve (2 messages, latest: Apr 13 2023 at 14:10)
• Simple things I can't get coq-interval to solve (9 messages, latest: Apr 13 2023 at 07:12)
• Tactic Showcase (2 messages, latest: Apr 12 2023 at 19:38)
• Coercion with implicit arguments (10 messages, latest: Apr 12 2023 at 16:54)
• Correctness of terms with existential variables (5 messages, latest: Apr 12 2023 at 14:54)
• Cubical Type Theory (13 messages, latest: Apr 12 2023 at 13:38)
• ✔ What is the difference between ind-ind and mut-ind (4 messages, latest: Apr 12 2023 at 08:27)
• What is the difference between ind-ind and mut-ind (1 message, latest: Apr 12 2023 at 07:55)
• even numbers (1 message, latest: Apr 11 2023 at 18:36)
• Ltac: throw fail in inner pattern matching (4 messages, latest: Apr 11 2023 at 15:33)
• lemma statement (4 messages, latest: Apr 11 2023 at 12:21)
• no similarity (7 messages, latest: Apr 11 2023 at 12:04)
• swap two points (2 messages, latest: Apr 11 2023 at 12:02)
• patteren matching (3 messages, latest: Apr 09 2023 at 08:02)
• avoid empty list (3 messages, latest: Apr 08 2023 at 11:24)
• LEM and de-Morgan's law (13 messages, latest: Apr 08 2023 at 10:47)
• Compare two infinite strings lexicographically (8 messages, latest: Apr 08 2023 at 09:10)
• Tiny proof without lia (17 messages, latest: Apr 07 2023 at 16:24)
• Debugging Canonical Structures (11 messages, latest: Apr 07 2023 at 12:50)
• same result (1 message, latest: Apr 06 2023 at 12:43)
• ✔ Conflicting notation & coercions weird interaction (1 message, latest: Apr 05 2023 at 19:56)
• Conflicting notation & coercions weird interaction (8 messages, latest: Apr 05 2023 at 09:45)
• Continuations in coq (8 messages, latest: Apr 05 2023 at 09:25)
• ✔ Ltac patten match on fixpoints (1 message, latest: Apr 04 2023 at 22:43)
• Ltac patten match on fixpoints (3 messages, latest: Apr 04 2023 at 17:42)
• ✔ Strict positivity problem (3 messages, latest: Apr 04 2023 at 06:55)
• Rewriting computational equivalences in SSReflect (12 messages, latest: Apr 04 2023 at 03:26)
• ✔ transport in pattern matching (4 messages, latest: Apr 02 2023 at 20:17)
• Two values of list (2 messages, latest: Mar 31 2023 at 08:23)
• both r equal (4 messages, latest: Mar 31 2023 at 08:20)
• equal to In (6 messages, latest: Mar 29 2023 at 20:44)
• Pointers on how to use type classes for using several monads (10 messages, latest: Mar 29 2023 at 16:36)
• equal values (2 messages, latest: Mar 28 2023 at 17:54)
• use of induction tactic (2 messages, latest: Mar 28 2023 at 17:50)
• contra conditions (6 messages, latest: Mar 28 2023 at 17:26)
• Which tactics manipulate the whole proof term? (7 messages, latest: Mar 28 2023 at 14:55)
• ✔ SSReflect equality problem (6 messages, latest: Mar 28 2023 at 14:26)
• Replacing a term in Dependent type without error (9 messages, latest: Mar 25 2023 at 16:00)
• GitHub is rolling out 2FA requirement (1 message, latest: Mar 25 2023 at 10:21)
• Proof with a subset type (11 messages, latest: Mar 24 2023 at 11:56)
• 4 color theorem preprint (1 message, latest: Mar 24 2023 at 11:34)
• use of tactic? (1 message, latest: Mar 24 2023 at 07:23)
• relation between numbers (4 messages, latest: Mar 23 2023 at 14:30)
• Did INSTALLDEFAULTROOT stop working in 8.15? (23 messages, latest: Mar 23 2023 at 12:21)
• use of destruct command (3 messages, latest: Mar 23 2023 at 10:58)
• github.com/yannl35133/coq rewrite rule nonlinear n ++ n ==>n (5 messages, latest: Mar 22 2023 at 17:15)
• Efficient raw input and output (72 messages, latest: Mar 21 2023 at 11:41)
• Representing mutual recursion functions (9 messages, latest: Mar 21 2023 at 10:31)
• revert function (2 messages, latest: Mar 20 2023 at 20:04)
• apply with Error: no such bound variable (4 messages, latest: Mar 20 2023 at 19:03)
• Notation for Explicit Arrays (35 messages, latest: Mar 20 2023 at 09:26)
• Proof strategy for UniMath `hexists` statements (2 messages, latest: Mar 20 2023 at 08:43)
• Top-down synthesis for library learning (4 messages, latest: Mar 20 2023 at 02:22)
• Use of In command (1 message, latest: Mar 19 2023 at 17:01)
• Collatz conjecture (4 messages, latest: Mar 17 2023 at 11:33)
• Variant vs Inductive (14 messages, latest: Mar 17 2023 at 11:29)
• Program Definiton use (5 messages, latest: Mar 17 2023 at 08:28)
• Get conclusion of implication with trivial hypothesis (7 messages, latest: Mar 16 2023 at 22:04)
• simlify list (2 messages, latest: Mar 16 2023 at 08:50)
• Parallel proof processing (4 messages, latest: Mar 15 2023 at 09:06)
• arrange elements (1 message, latest: Mar 14 2023 at 18:10)
• help in Coq (1 message, latest: Mar 14 2023 at 15:09)
• Vscode ssh (3 messages, latest: Mar 14 2023 at 11:02)
• Record Set and sub-records (2 messages, latest: Mar 13 2023 at 22:11)
• UniMath Category theory basics (8 messages, latest: Mar 13 2023 at 15:03)
• Primitive projection (3 messages, latest: Mar 13 2023 at 10:47)
• Jump instr and infinite loop (14 messages, latest: Mar 13 2023 at 07:30)
• meaning of statement (5 messages, latest: Mar 12 2023 at 18:05)
• nth element on coquelicot Tn sequence (7 messages, latest: Mar 12 2023 at 15:54)
• elements mismatch (6 messages, latest: Mar 12 2023 at 15:12)
• rec and rect (6 messages, latest: Mar 12 2023 at 09:15)
• Enumerating Dyck words (11 messages, latest: Mar 11 2023 at 17:15)
• conditions (1 message, latest: Mar 11 2023 at 15:50)
• same patteren (22 messages, latest: Mar 11 2023 at 12:09)
• list is empty or not (6 messages, latest: Mar 09 2023 at 13:44)
• An issue with the ! flag in the Arguments command (22 messages, latest: Mar 08 2023 at 10:48)
• Help from H (4 messages, latest: Mar 08 2023 at 08:18)
• ✔ Creating new hypothesis using Ltac (4 messages, latest: Mar 08 2023 at 03:43)
• On the art of fixing the universe (30 messages, latest: Mar 07 2023 at 11:12)
• Easycrypt (1 message, latest: Mar 07 2023 at 09:28)
• Contravariant subtyping (13 messages, latest: Mar 07 2023 at 07:43)
• Coq can't recognize a strictly positive occurrence (7 messages, latest: Mar 06 2023 at 07:48)
• constructor (6 messages, latest: Mar 05 2023 at 08:58)
• ✔ Problem with recursive pattern in notations (2 messages, latest: Mar 03 2023 at 18:29)
• false statement (2 messages, latest: Mar 03 2023 at 18:27)
• Error When Installing Coq from OPAM(RHEL 8.7) (32 messages, latest: Mar 03 2023 at 08:33)
• Make a definition opaque for rewrite? (5 messages, latest: Mar 02 2023 at 20:14)
• Type theory (5 messages, latest: Mar 02 2023 at 19:55)
• Performance Debugging Typeclass Resolution (15 messages, latest: Mar 01 2023 at 22:46)
• Proof with inequality and false assumption (5 messages, latest: Mar 01 2023 at 10:17)
• Mutually inducting to show decidable equality (34 messages, latest: Feb 28 2023 at 09:54)
• simpl on own type (20 messages, latest: Feb 27 2023 at 17:05)
• Extraction to mixed haskell/ocaml (9 messages, latest: Feb 27 2023 at 14:54)
• Utf8 strings in coq? (13 messages, latest: Feb 27 2023 at 10:08)
• Coercion with implicit Type -> Type works, fails for Type (6 messages, latest: Feb 27 2023 at 01:47)
• both possibilities exist? (8 messages, latest: Feb 26 2023 at 17:33)
• list nat (11 messages, latest: Feb 26 2023 at 17:22)
• Using `Function` for recursion (13 messages, latest: Feb 25 2023 at 12:56)
• Ltac for set-theoretical reasoning (3 messages, latest: Feb 24 2023 at 19:46)
• is there contradiction? (3 messages, latest: Feb 24 2023 at 18:10)
• Notation with binder only in part of the right-hand side (7 messages, latest: Feb 24 2023 at 12:28)
• As intro pattern (6 messages, latest: Feb 24 2023 at 11:59)
• Compiling Coq Standard Library (12 messages, latest: Feb 23 2023 at 20:03)
• false case (2 messages, latest: Feb 22 2023 at 17:13)
• How to Debug slow QED? (146 messages, latest: Feb 22 2023 at 12:44)
• Varieties (12 messages, latest: Feb 22 2023 at 11:57)
• Proof with BinNat and xor (3 messages, latest: Feb 21 2023 at 22:08)
• How to do induction with stronger assumption? (29 messages, latest: Feb 20 2023 at 11:04)
• extract information (4 messages, latest: Feb 19 2023 at 19:24)
• Difference between two commands (3 messages, latest: Feb 19 2023 at 08:14)
• solve by lia (7 messages, latest: Feb 18 2023 at 14:10)
• is it right way of writing? (1 message, latest: Feb 18 2023 at 11:35)
• what is clib (3 messages, latest: Feb 16 2023 at 20:47)
• Proof View dump (5 messages, latest: Feb 16 2023 at 19:19)
• ✔ Redefining a built-in tactic (3 messages, latest: Feb 16 2023 at 14:17)
• is there a tactic for automating left/right. (4 messages, latest: Feb 14 2023 at 21:25)
• Proving the existence of a coinductive term (5 messages, latest: Feb 14 2023 at 14:05)
• Error: Cannot access opaque delayed proof (17 messages, latest: Feb 13 2023 at 20:00)
• Built in way to convert string to nat (or positive) (7 messages, latest: Feb 12 2023 at 16:58)
• jscoq saving and reloading (1 message, latest: Feb 11 2023 at 21:58)
• bypass_check(guard) in section (5 messages, latest: Feb 10 2023 at 07:52)
• directory structure for a PL project (17 messages, latest: Feb 09 2023 at 22:35)
• Coq in high school (53 messages, latest: Feb 09 2023 at 18:12)
• apply destruct (2 messages, latest: Feb 09 2023 at 16:00)
• destruct command (3 messages, latest: Feb 09 2023 at 15:10)
• ✔ Nix flake setup (11 messages, latest: Feb 08 2023 at 16:20)
• CompCert CI (27 messages, latest: Feb 08 2023 at 14:50)
• Primitive projection wrapping (32 messages, latest: Feb 08 2023 at 13:32)
• Refolding of definitions (1 message, latest: Feb 07 2023 at 15:00)
• alternate way of writing (2 messages, latest: Feb 07 2023 at 13:37)
• ✔ Coq 8.17 is *fast* (9 messages, latest: Feb 06 2023 at 18:12)
• Convincing Coq accept my definition (35 messages, latest: Feb 06 2023 at 15:00)
• existence (1 message, latest: Feb 04 2023 at 18:11)
• ✔ One final lemma (10 messages, latest: Feb 03 2023 at 13:57)
• execute example (2 messages, latest: Feb 03 2023 at 11:13)
• How to write incremental modular coq code (11 messages, latest: Feb 02 2023 at 14:32)
• Multiple binders (5 messages, latest: Jan 31 2023 at 23:13)
• GitHub tarball checksum changes (2 messages, latest: Jan 30 2023 at 22:37)
• how to modify code (6 messages, latest: Jan 30 2023 at 16:46)
• Help with syntax (9 messages, latest: Jan 30 2023 at 15:55)
• What does this production in the binder grammar mean? (3 messages, latest: Jan 29 2023 at 01:10)
• VSCoq extension for VSCode doesn't work (1 message, latest: Jan 25 2023 at 12:51)
• Difference between Induction and Elimination Schemes (2 messages, latest: Jan 25 2023 at 12:33)
• Random selection (14 messages, latest: Jan 25 2023 at 04:27)
• How to reuse code / modularize (9 messages, latest: Jan 24 2023 at 16:06)
• Alternative way to install Coq Platform (1 message, latest: Jan 24 2023 at 08:59)
• A wild exchange argument just landed! (4 messages, latest: Jan 23 2023 at 20:02)
• Problem with CPDT's dependent list examples (15 messages, latest: Jan 23 2023 at 12:19)
• How to simplify? (10 messages, latest: Jan 22 2023 at 12:37)
• How to deal with proof irrelevance (16 messages, latest: Jan 22 2023 at 12:20)
• problem in storing elements in list (1 message, latest: Jan 22 2023 at 08:11)
• advancingIsAlwaysOk (23 messages, latest: Jan 21 2023 at 19:04)
• conversion (13 messages, latest: Jan 21 2023 at 15:11)
• Coercions in proofs (15 messages, latest: Jan 20 2023 at 23:46)
• Coq State Machine Plans (2 messages, latest: Jan 19 2023 at 21:14)
• rewriting with PERs (28 messages, latest: Jan 19 2023 at 16:01)
• listsEqual tactic (6 messages, latest: Jan 19 2023 at 15:10)
• Extraction wierd behavriour (7 messages, latest: Jan 19 2023 at 09:23)
• Review regular bracket string proof (8 messages, latest: Jan 17 2023 at 14:32)
• Regex library for research (6 messages, latest: Jan 16 2023 at 07:35)
• ✔ proving inequality by induction? (6 messages, latest: Jan 15 2023 at 14:10)
• Terms as Coercions (9 messages, latest: Jan 13 2023 at 09:50)
• ✔ Forcing reduction of record map (7 messages, latest: Jan 12 2023 at 21:10)
• Coq equation's equivalent of `Set Program Cases` (1 message, latest: Jan 11 2023 at 16:37)
• Help for Heterogenous vector (30 messages, latest: Jan 11 2023 at 10:19)
• ✔ Why lia won't solve this goal? (11 messages, latest: Jan 11 2023 at 09:04)
• opam install coq fails with "flock: permission denied" (60 messages, latest: Jan 11 2023 at 03:50)
• Whatis induction-recursion? (29 messages, latest: Jan 09 2023 at 23:50)
• ✔ Disabling Local Notation in a Coq file (5 messages, latest: Jan 09 2023 at 13:43)
• ✔ Silencing notation-overriden warning (3 messages, latest: Jan 09 2023 at 13:43)
• Project File Problem (4 messages, latest: Jan 08 2023 at 08:39)
• SIGSEGV on extracted code (24 messages, latest: Jan 05 2023 at 07:59)
• "Read-only file system" on opam install (14 messages, latest: Jan 05 2023 at 01:21)
• Use of In prdicate (3 messages, latest: Jan 04 2023 at 16:01)
• anti-unification (1 message, latest: Jan 04 2023 at 14:53)
• Coq-Ci needs full CI (1 message, latest: Jan 04 2023 at 09:55)
• ✔ Ltac: push internal subgoal to the user (14 messages, latest: Jan 04 2023 at 08:41)
• RelationPairs rewriting really slow (6 messages, latest: Jan 03 2023 at 18:50)
• How do nested _CoqProjects and Makefiles work? (8 messages, latest: Jan 03 2023 at 13:45)
• ✔ Rewrite gets stuck (7 messages, latest: Dec 30 2022 at 23:54)
• ✔ What's wrong with my `meta.yml`? (8 messages, latest: Dec 29 2022 at 09:35)
• ✔ What is this notation? (6 messages, latest: Dec 29 2022 at 06:36)
• Cost of automatic tactics during compilation (41 messages, latest: Dec 25 2022 at 13:41)
• Eliminate Prop in a Prop (6 messages, latest: Dec 22 2022 at 12:50)
• Notation for unpacking a value (3 messages, latest: Dec 21 2022 at 13:24)
• Inductive relation over another relation (19 messages, latest: Dec 21 2022 at 10:31)
• Jupyter/Notebook integration (7 messages, latest: Dec 19 2022 at 14:21)
• `Print Module` using types from body instead of sealing (2 messages, latest: Dec 19 2022 at 14:21)
• ✔ How to get rid of unnecessary existential variables? (4 messages, latest: Dec 18 2022 at 10:26)
• Triple in Function (2 messages, latest: Dec 16 2022 at 18:48)
• Fixpoint to test if a list is ordered (5 messages, latest: Dec 14 2022 at 14:41)
• ✔ Is True a neutral element for and? (8 messages, latest: Dec 14 2022 at 12:13)
• Standard way to parse float-like numbers? (6 messages, latest: Dec 13 2022 at 13:24)
• SProp Setoid Rewriting (1 message, latest: Dec 11 2022 at 23:16)
• SProp Unification Failure (9 messages, latest: Dec 11 2022 at 18:32)
• Convince coq that a function decreases argument (7 messages, latest: Dec 11 2022 at 12:06)
• wrong statement (5 messages, latest: Dec 10 2022 at 17:57)
• alternate (3 messages, latest: Dec 10 2022 at 17:33)
• false relation (3 messages, latest: Dec 09 2022 at 18:36)
• theorem statement (1 message, latest: Dec 09 2022 at 03:54)
• List.filter respects Setoid Equality (equivlistA) (4 messages, latest: Dec 08 2022 at 09:31)
• ✔ Typeclass instance for mutually inductive types (7 messages, latest: Dec 07 2022 at 01:25)
• ✔ binary logarithm on nat (5 messages, latest: Dec 05 2022 at 08:12)
• Canonical structures frustration (13 messages, latest: Dec 05 2022 at 07:57)
• Exporting proof term (7 messages, latest: Dec 03 2022 at 11:17)
• Controlling printing notations (17 messages, latest: Dec 03 2022 at 03:17)
• Using HoTT Library (74 messages, latest: Dec 02 2022 at 18:35)
• ✔ A PHOAS example (8 messages, latest: Dec 02 2022 at 10:35)
• Induction Principal for Set, represented by list. (4 messages, latest: Dec 01 2022 at 09:42)
• No of elements (3 messages, latest: Dec 01 2022 at 07:21)
• Change, but with evars (22 messages, latest: Nov 29 2022 at 20:01)
• ✔ beginners question on induction (20 messages, latest: Nov 29 2022 at 13:32)
• Coq gets killed (9 messages, latest: Nov 29 2022 at 13:08)
• Some Coq servers down (2 messages, latest: Nov 29 2022 at 12:15)
• Combining typeclasses and recursion (25 messages, latest: Nov 27 2022 at 23:05)
• Quantifying over Type and remaining in Prop (8 messages, latest: Nov 26 2022 at 17:53)
• z <= 1000 (4 messages, latest: Nov 26 2022 at 16:20)
• Coq's guard condition (19 messages, latest: Nov 24 2022 at 21:55)
• Setoid rewrite with no init (14 messages, latest: Nov 24 2022 at 18:56)
• Obj.magic for Coq?! (20 messages, latest: Nov 24 2022 at 15:36)
• .coqrc in coqc (4 messages, latest: Nov 24 2022 at 15:22)
• I am struggling to understand well_founded (12 messages, latest: Nov 24 2022 at 14:57)
• Coercion syntax (5 messages, latest: Nov 23 2022 at 17:08)
• VsCode Issue (1 message, latest: Nov 23 2022 at 07:29)
• `Proper ... (Under_rel ...)` (6 messages, latest: Nov 22 2022 at 21:54)
• rewriting under binder in ssreflect style rewrite. (12 messages, latest: Nov 22 2022 at 19:36)
• forward reasoning (14 messages, latest: Nov 22 2022 at 09:36)
• ✔ logical xor (11 messages, latest: Nov 21 2022 at 17:56)
• Connect PG / VsCoq to docker? (15 messages, latest: Nov 21 2022 at 11:11)
• Universe instance i+1 (3 messages, latest: Nov 21 2022 at 10:42)
• is_evar tactic (1 message, latest: Nov 18 2022 at 14:42)
• Problem with nested fixpoints (15 messages, latest: Nov 18 2022 at 01:58)
• Notations for typing relations (7 messages, latest: Nov 17 2022 at 19:13)
• new bug in cannonical structures? (45 messages, latest: Nov 16 2022 at 20:05)
• coqdoc custom css (8 messages, latest: Nov 16 2022 at 00:35)
• ProofGeneral release 4.5 (5 messages, latest: Nov 14 2022 at 15:49)
• match with sigma type problem (5 messages, latest: Nov 12 2022 at 21:37)
• indexed modules (2 messages, latest: Nov 10 2022 at 20:14)
• ✔ need some help with a simpl proof (5 messages, latest: Nov 10 2022 at 06:21)
• learning Coq (3 messages, latest: Nov 09 2022 at 15:19)
• Can we rewrite using this type (10 messages, latest: Nov 09 2022 at 07:52)
• make validate / coqchk lists axioms that were not used (11 messages, latest: Nov 08 2022 at 23:50)
• How to do simplification of expression correctly (?) (14 messages, latest: Nov 07 2022 at 16:21)
• Tactic notation and custom entries (12 messages, latest: Nov 07 2022 at 15:54)
• Evaluate suitably a `fix` to explicit an internal fixpoint (3 messages, latest: Nov 06 2022 at 23:27)
• Typeclass resolution algorithm? (32 messages, latest: Nov 05 2022 at 16:10)
• Opaque inductive type (9 messages, latest: Nov 05 2022 at 13:13)
• Regex representation (39 messages, latest: Nov 05 2022 at 07:47)
• ✔ Complex induction principles (8 messages, latest: Nov 04 2022 at 19:35)
• How to resolve this? (2 messages, latest: Nov 04 2022 at 17:49)
• Dealing with injection with Impredicative Set (7 messages, latest: Nov 04 2022 at 13:32)
• Tactic with optional parameter (20 messages, latest: Nov 03 2022 at 22:58)
• CoqIDE: store preferences does not work on Mac (5 messages, latest: Nov 03 2022 at 10:44)
• PrimFloat binary representation (9 messages, latest: Nov 02 2022 at 10:51)
• Library Code (9 messages, latest: Nov 02 2022 at 08:22)
• ✔ Dependent Pattern Match -- Unification (11 messages, latest: Nov 02 2022 at 04:06)
• Convertability and Typing of Terms (14 messages, latest: Nov 01 2022 at 23:18)
• Request for Comments/ Code review (1 message, latest: Nov 01 2022 at 16:41)
• Pencil and Paper Coq Course (4 messages, latest: Nov 01 2022 at 13:46)
• eq-refl (2 messages, latest: Nov 01 2022 at 13:42)
• ✔ auto bug / strange behavior (5 messages, latest: Nov 01 2022 at 13:30)
• ✔ /\\ typo or real syntax? (5 messages, latest: Nov 01 2022 at 01:04)
• Multimatch in auto (2 messages, latest: Nov 01 2022 at 00:58)
• Hint Cut with Hint Extern? (1 message, latest: Oct 31 2022 at 23:06)
• `Typeclasses Dependency Order` (5 messages, latest: Oct 31 2022 at 23:02)
• Overriding stdlib pairs (9 messages, latest: Oct 31 2022 at 13:04)
• Proving properties of Field (5 messages, latest: Oct 31 2022 at 10:09)
• Debug long Qed or Defined (2 messages, latest: Oct 31 2022 at 08:51)
• Automatically apply with coercion (1 message, latest: Oct 30 2022 at 15:24)
• Counting number of certain branches executed in Ltac (5 messages, latest: Oct 30 2022 at 13:37)
• Canonical structures for depenent types (5 messages, latest: Oct 30 2022 at 08:06)
• ✔ How to hide definitions of propositions? (12 messages, latest: Oct 29 2022 at 09:03)
• ✔ Notation In Coq'Art (4 messages, latest: Oct 29 2022 at 06:56)
• ✔ question about eqv to eq (9 messages, latest: Oct 28 2022 at 22:57)
• Struggle with using canonical structures mathcomp style (17 messages, latest: Oct 28 2022 at 20:11)
• ✔ Simple Question on the structure of Coq (4 messages, latest: Oct 28 2022 at 18:59)
• How to build a record using tactics language (14 messages, latest: Oct 28 2022 at 13:01)
• Unguarded recursive calls (5 messages, latest: Oct 27 2022 at 09:55)
• No implementations provided for Coq Modules (15 messages, latest: Oct 27 2022 at 09:53)
• ✔ Library-wise unsafe coqc mode (5 messages, latest: Oct 26 2022 at 18:16)
• How to restore windows in proof general? (1 message, latest: Oct 26 2022 at 16:41)
• ✔ Autosubst (2) (7 messages, latest: Oct 26 2022 at 12:42)
• Failure of the tactic inductive ... using (21 messages, latest: Oct 26 2022 at 09:18)
• derive contra statement (9 messages, latest: Oct 26 2022 at 08:48)
• short form (7 messages, latest: Oct 25 2022 at 04:38)
• Coq Module Extraction Issue (ocaml extraction bug?) (3 messages, latest: Oct 25 2022 at 00:45)
• Students interviewing about Program Verification IDEs (6 messages, latest: Oct 24 2022 at 16:54)
• ✔ Encoding a Prop Inductive in Type (31 messages, latest: Oct 24 2022 at 13:40)
• Simpl/ ssreflect and cbv iota fail to simplify a fixpoint (5 messages, latest: Oct 23 2022 at 21:49)
• Can Coq generate nicely styled documentation for markdown (2 messages, latest: Oct 21 2022 at 12:31)
• How to instantiate existential variable in the context (4 messages, latest: Oct 20 2022 at 20:29)
• Proofweb (2 messages, latest: Oct 20 2022 at 07:40)
• Is there way to use lia with ssreflect? (2 messages, latest: Oct 20 2022 at 01:30)
• Strange rewrite failure (12 messages, latest: Oct 19 2022 at 17:21)
• Typeclasses (5 messages, latest: Oct 19 2022 at 17:15)
• Recreating unification of apply and rewrite (1 message, latest: Oct 19 2022 at 15:55)
• When to use `==` and when to use `=` in ssreflect (7 messages, latest: Oct 19 2022 at 15:41)
• How does `Extraction` decide the naming scheme? (1 message, latest: Oct 17 2022 at 16:43)
• 2 questions about ssreflect (12 messages, latest: Oct 17 2022 at 11:13)
• Any certified C library for unlimited precision integers? (5 messages, latest: Oct 17 2022 at 07:26)
• exact vs apply tactic? (8 messages, latest: Oct 16 2022 at 13:45)
• ✔ Searching for tactic (4 messages, latest: Oct 16 2022 at 11:40)
• ✔ Assert member of one type is member of another (5 messages, latest: Oct 16 2022 at 07:20)
• ✔ How can I say that variables satisfy certain typeclass? (13 messages, latest: Oct 14 2022 at 22:12)
• Quotient types (2 messages, latest: Oct 14 2022 at 20:38)
• Is lia helpful here? (4 messages, latest: Oct 14 2022 at 17:23)
• Dependent types of applicative functions? (14 messages, latest: Oct 14 2022 at 12:54)
• ✔ Complicated dependent types (4 messages, latest: Oct 13 2022 at 12:30)
• Project nth element of n-tuple (15 messages, latest: Oct 13 2022 at 08:41)
• ✔ Term mode and tactic mode (4 messages, latest: Oct 13 2022 at 00:11)
• Simplifying CoFixpoints (15 messages, latest: Oct 12 2022 at 16:56)
• ✔ Destruct on inductive types (17 messages, latest: Oct 12 2022 at 15:42)
• ✔ Empty context in ltac (6 messages, latest: Oct 12 2022 at 13:28)
• ✔ How to get rid of duplicate goals (7 messages, latest: Oct 12 2022 at 12:18)
• ✔ Using `auto` tactic (5 messages, latest: Oct 12 2022 at 09:54)
• Phishing on Coq-Club (8 messages, latest: Oct 12 2022 at 09:48)
• Multiple aliases for nat that does not mix (6 messages, latest: Oct 10 2022 at 15:11)
• what is SSReflect about? (11 messages, latest: Oct 10 2022 at 07:35)
• Why does this rewrite fail ? (9 messages, latest: Oct 09 2022 at 22:31)
• Coq and assembler (6 messages, latest: Oct 09 2022 at 12:48)
• ✔ Small typo in warning (3 messages, latest: Oct 08 2022 at 20:41)
• Escape [ for coqdoc? (5 messages, latest: Oct 08 2022 at 09:19)
• Some Questions on Extraction (13 messages, latest: Oct 07 2022 at 20:22)
• ✔ Context match bug (24 messages, latest: Oct 07 2022 at 19:24)
• `if` vs `match` in printing, `case_style` (1 message, latest: Oct 07 2022 at 17:48)
• Command to know if notation is left or right assoc ? (12 messages, latest: Oct 07 2022 at 12:06)
• Having trouble installing Coq with opam (5 messages, latest: Oct 07 2022 at 09:26)
• Ltac2 learning resources (1 message, latest: Oct 06 2022 at 21:33)
• Using Streams.Exists (10 messages, latest: Oct 06 2022 at 09:12)
• Number theory libraries (3 messages, latest: Oct 06 2022 at 07:20)
• ✔ Induction principle (8 messages, latest: Oct 06 2022 at 01:29)
• JMeq and functions (26 messages, latest: Oct 05 2022 at 14:32)
• Coq FAQ in wiki (8 messages, latest: Oct 05 2022 at 11:03)
• ✔ Just proving some lemmas... (17 messages, latest: Oct 04 2022 at 12:39)
• ✔ Partial auto (11 messages, latest: Oct 04 2022 at 10:59)
• ✔ Using short names of theorems in a Module (eg PeanoNat.... (6 messages, latest: Oct 04 2022 at 05:50)
• ✔ pattern matching question (36 messages, latest: Oct 04 2022 at 05:05)
• LTAC vs LTAC2 (11 messages, latest: Oct 03 2022 at 08:52)
• ✔ IDE support for Dune (32 messages, latest: Sep 30 2022 at 16:27)
• ✔ Printing of primitive floats (27 messages, latest: Sep 30 2022 at 15:49)
• ✔ Find term of a given type (4 messages, latest: Sep 29 2022 at 13:31)
• Code typechecks in Coq 8.13, but not in 8.14 (16 messages, latest: Sep 28 2022 at 20:29)
• SF lecture videos (3 messages, latest: Sep 28 2022 at 20:22)
• ✔ New project (7 messages, latest: Sep 27 2022 at 15:42)
• Extracting to a directory (20 messages, latest: Sep 27 2022 at 11:39)
• ✔ coqtop is not running (15 messages, latest: Sep 27 2022 at 10:14)
• ✔ Lost in Tactic Notation (8 messages, latest: Sep 26 2022 at 20:47)
• ✔ Stuck with Program Fixpoint (46 messages, latest: Sep 26 2022 at 20:34)
• Scheme Boolean Equality and types as parameters in a section (17 messages, latest: Sep 26 2022 at 13:38)
• Coq in VS Code (1 message, latest: Sep 25 2022 at 16:14)
• ✔ Is it possible to make simpl automatically unfold defin... (10 messages, latest: Sep 25 2022 at 14:28)
• ✔ Good coding practices for coq (7 messages, latest: Sep 25 2022 at 13:32)
• Understanding subset type (8 messages, latest: Sep 25 2022 at 11:21)
• ✔ ssreflect (6 messages, latest: Sep 25 2022 at 08:52)
• Avoiding loops with auto (11 messages, latest: Sep 24 2022 at 11:28)
• Operation on Functions (12 messages, latest: Sep 23 2022 at 22:19)
• variable relation? (17 messages, latest: Sep 23 2022 at 14:02)
• Add auto hint per Lemma (2 messages, latest: Sep 22 2022 at 21:53)
• Is there ready to uses lemmas for MsetAVL. (11 messages, latest: Sep 21 2022 at 20:27)
• How to substitute MSets.MSetAVL that are `Equal`s (5 messages, latest: Sep 21 2022 at 19:44)
• succ of number (10 messages, latest: Sep 21 2022 at 01:04)
• ✔ Append of two length-indexed vectors does not type-check (4 messages, latest: Sep 20 2022 at 18:58)
• Probability Monad for Fin.t (41 messages, latest: Sep 20 2022 at 15:01)
• ✔ Balanced bracket strings (7 messages, latest: Sep 20 2022 at 06:59)
• Is there a tactice that disprove constructors are equal (15 messages, latest: Sep 19 2022 at 14:29)
• Fixpoint termination (29 messages, latest: Sep 19 2022 at 14:20)
• Isn't this a contradiction (20 messages, latest: Sep 17 2022 at 15:54)
• ✔ Hypothesis in if then else (7 messages, latest: Sep 16 2022 at 13:51)
• lia shows error. (8 messages, latest: Sep 15 2022 at 13:56)
• Multiple Proofs (31 messages, latest: Sep 15 2022 at 13:00)
• ✔ Proof: Sum of even nos is even (6 messages, latest: Sep 15 2022 at 12:11)
• Custom reduction (16 messages, latest: Sep 14 2022 at 14:41)
• Is there a way to represent Intervals as inductive types? (3 messages, latest: Sep 13 2022 at 11:16)
• ✔ Rust Extraction (46 messages, latest: Sep 13 2022 at 10:44)
• Simplify the arguments of a constructor (2 messages, latest: Sep 13 2022 at 05:23)
• Tactic that looks like a function (3 messages, latest: Sep 12 2022 at 17:32)
• Extracting Functor typeclass to Haskell (5 messages, latest: Sep 12 2022 at 13:36)
• Proving a Real number inequality (3 messages, latest: Sep 12 2022 at 06:02)
• ✔ Formalize a game (10 messages, latest: Sep 11 2022 at 06:01)
• One less than other (9 messages, latest: Sep 10 2022 at 04:55)
• ✔ Counting operations used by a function (6 messages, latest: Sep 09 2022 at 16:54)
• ✔ Non-terminating/super-slow unification (39 messages, latest: Sep 08 2022 at 20:39)
• Basic integration (5 messages, latest: Sep 08 2022 at 15:07)
• Symbol management functions (1 message, latest: Sep 08 2022 at 14:00)
• ✔ How do I debug Ltac being stuck? (7 messages, latest: Sep 08 2022 at 00:45)
• ✔ Coq extraction: Pervasives is deprecated (9 messages, latest: Sep 07 2022 at 19:39)
• ✔ "Overloading" notation of inductives using typeclasses (11 messages, latest: Sep 07 2022 at 17:48)
• ✔ admit until later (5 messages, latest: Sep 07 2022 at 10:03)
• Windows parsing change (1 message, latest: Sep 06 2022 at 22:02)
• ✔ Weakness in FMaps (7 messages, latest: Sep 06 2022 at 12:42)
• extract info (23 messages, latest: Sep 06 2022 at 08:15)
• ✔ Nested recursion (7 messages, latest: Sep 05 2022 at 12:56)
• Register section variable as a type class (2 messages, latest: Sep 05 2022 at 12:13)
• Floating point computations (15 messages, latest: Sep 05 2022 at 09:39)
• ✔ Infinite list (4 messages, latest: Sep 05 2022 at 09:19)
• How do you connect to Coq IDE (standalone) for XML? (6 messages, latest: Sep 05 2022 at 07:32)
• Extraction: nat to Integer (Haskell) (4 messages, latest: Sep 03 2022 at 16:37)
• Ltac: abstracting over pattern? (14 messages, latest: Sep 02 2022 at 14:13)
• Two different data types (1 message, latest: Sep 01 2022 at 03:39)
• Hint pattern beginner question (2 messages, latest: Aug 31 2022 at 20:01)
• Set vs Type (6 messages, latest: Aug 31 2022 at 17:50)
• Applying Functors multiple times (23 messages, latest: Aug 31 2022 at 16:37)
• [Beginner] Differences between Coq and Gallina (123 messages, latest: Aug 31 2022 at 14:50)
• error removal (2 messages, latest: Aug 31 2022 at 11:01)
• help from library (4 messages, latest: Aug 30 2022 at 18:44)
• ✔ Run a tactic on all hypothesis once (5 messages, latest: Aug 30 2022 at 15:30)
• ✔ Extraction: Haskell type constraints (7 messages, latest: Aug 30 2022 at 05:58)
• Extracting type with 2 args to Haskell (3 messages, latest: Aug 29 2022 at 07:20)
• Coq and semantics (9 messages, latest: Aug 27 2022 at 19:29)
• Array Theory (11 messages, latest: Aug 27 2022 at 12:59)
• ✔ Me being illiterate (in programming) (33 messages, latest: Aug 26 2022 at 21:10)
• writing error ? (1 message, latest: Aug 25 2022 at 15:50)
• Extracting coq-ext-lib fmap to haskell (2 messages, latest: Aug 25 2022 at 09:44)
• ✔ Extracting record type (6 messages, latest: Aug 25 2022 at 04:24)
• plus versus add (10 messages, latest: Aug 24 2022 at 13:31)
• ✔ fmap in coq-ext-lib (7 messages, latest: Aug 24 2022 at 09:37)
• ✔ Function with dependently-typed result type (PnP exercise) (9 messages, latest: Aug 24 2022 at 02:24)
• Tactic to return the whole goal? (2 messages, latest: Aug 24 2022 at 02:17)
• ✔ Puzzling error with dependent types (7 messages, latest: Aug 23 2022 at 19:53)
• how Coq treats values vs every other programming language (14 messages, latest: Aug 17 2022 at 10:23)
• ✔ View patterns (6 messages, latest: Aug 16 2022 at 13:51)
• Choosing notation level (4 messages, latest: Aug 16 2022 at 12:27)
• What is `RInv R0` (5 messages, latest: Aug 16 2022 at 12:02)
• How to find length (11 messages, latest: Aug 16 2022 at 07:38)
• How to make simple? (1 message, latest: Aug 16 2022 at 07:29)
• ✔ Program Fixpoint measure - simple example (29 messages, latest: Aug 14 2022 at 14:31)
• Does Coq have equivalent for Ocaml's `match ... when` (3 messages, latest: Aug 12 2022 at 17:42)
• Codewars requirements for Coq (16 messages, latest: Aug 12 2022 at 11:57)
• ✔ Correctly unfold function definition (5 messages, latest: Aug 12 2022 at 08:44)
• ✔ Recursion + mutual recursion (7 messages, latest: Aug 11 2022 at 22:25)
• Relation with hypothesis (1 message, latest: Aug 11 2022 at 17:29)
• Auto-fix for future-coercion-class-field? (13 messages, latest: Aug 11 2022 at 16:15)
• QuickChick anomaly (11 messages, latest: Aug 11 2022 at 12:53)
• How to revert a tactic (3 messages, latest: Aug 11 2022 at 10:48)
• Record update (5 messages, latest: Aug 10 2022 at 22:59)
• Universe-polymorphic module types and modules (12 messages, latest: Aug 10 2022 at 20:01)
• Any hints how to prove injectivity? (21 messages, latest: Aug 10 2022 at 14:24)
• ✔ Contents of a typed module (7 messages, latest: Aug 10 2022 at 10:04)
• HashMap or equivalent impelementation? (5 messages, latest: Aug 09 2022 at 22:40)
• ✔ change with checked type (7 messages, latest: Aug 09 2022 at 12:31)
• Partial maps and id's (3 messages, latest: Aug 08 2022 at 08:15)
• ✔ Stuck with a seemingly simple proof. (6 messages, latest: Aug 08 2022 at 07:07)
• which one is greater (13 messages, latest: Aug 08 2022 at 05:34)
• How to explore Coq API (44 messages, latest: Aug 07 2022 at 22:33)
• What is the keyword Set ? (8 messages, latest: Aug 06 2022 at 14:02)
• natural number counting (2 messages, latest: Aug 05 2022 at 18:48)
• less than relation (4 messages, latest: Aug 05 2022 at 18:29)
• ✔ Question about lia (20 messages, latest: Aug 05 2022 at 18:16)
• Competitive programmers (15 messages, latest: Aug 05 2022 at 16:42)
• Beautify (5 messages, latest: Aug 04 2022 at 17:42)
• ✔ Notation in section (3 messages, latest: Aug 04 2022 at 10:53)
• ✔ Why variable is not substituted? (5 messages, latest: Aug 03 2022 at 11:31)
• Work with sets (5 messages, latest: Aug 03 2022 at 09:22)
• Translating expressions between languages (4 messages, latest: Aug 03 2022 at 08:40)
• Is wrong statement ? (3 messages, latest: Aug 03 2022 at 08:34)
• ✔ Matching Gallina's `let .. in` with Ltac (7 messages, latest: Aug 03 2022 at 07:56)
• How to prove countability of formulas? (4 messages, latest: Aug 03 2022 at 07:20)
• Defining a fold left induction principle (10 messages, latest: Aug 03 2022 at 05:14)
• diffenent form (3 messages, latest: Aug 02 2022 at 18:18)
• Greater or less relation (10 messages, latest: Aug 02 2022 at 18:18)
• A technical question when reading the mathcomp book (2 messages, latest: Aug 02 2022 at 11:24)
• ✔ Cantor pairing function and countability (10 messages, latest: Aug 01 2022 at 17:08)
• Extract to a variable file name (1 message, latest: Aug 01 2022 at 15:05)
• Haskell extraction with type constraints (9 messages, latest: Aug 01 2022 at 11:55)
• ✔ Recursion principle for tree (4 messages, latest: Jul 31 2022 at 09:15)
• what are mlg files? (11 messages, latest: Jul 30 2022 at 13:03)
• From successor (7 messages, latest: Jul 30 2022 at 06:20)
• ✔ Show theorem name tactic. (3 messages, latest: Jul 29 2022 at 19:26)
• ✔ how to prove this in Coq (10 messages, latest: Jul 29 2022 at 06:15)
• Extraction: Inductive type with args (5 messages, latest: Jul 28 2022 at 07:46)
• Alternatives to VST (47 messages, latest: Jul 27 2022 at 23:31)
• How to define small tactics inside a proof? (4 messages, latest: Jul 27 2022 at 02:55)
• Ex Lean user learning Coq (23 messages, latest: Jul 26 2022 at 15:49)
• Induction scheme for a range of Z (36 messages, latest: Jul 26 2022 at 09:17)
• Set union (3 messages, latest: Jul 24 2022 at 08:53)
• Declare variable (13 messages, latest: Jul 23 2022 at 16:11)
• ✔ [Beginner theory] Are Coq tactics a deductive system? (8 messages, latest: Jul 23 2022 at 14:04)
• Large inductive example from CPDT accepte (27 messages, latest: Jul 22 2022 at 15:07)
• ordered data structure? (33 messages, latest: Jul 22 2022 at 10:29)
• Word libraries and duplication (19 messages, latest: Jul 21 2022 at 11:44)
• Coq Art Exercise (20 messages, latest: Jul 20 2022 at 13:02)
• ✔ Extracting function to 3rd party function (5 messages, latest: Jul 20 2022 at 05:21)
• Equality in count_occ (4 messages, latest: Jul 19 2022 at 22:13)
• ✔ tree membership prop (6 messages, latest: Jul 17 2022 at 21:33)
• Total elements (2 messages, latest: Jul 17 2022 at 19:35)
• Discharging power mod proof (10 messages, latest: Jul 17 2022 at 09:34)
• More like a math question, but still (49 messages, latest: Jul 16 2022 at 22:23)
• ✔ I forgot how to tell Coq that two types are equal (4 messages, latest: Jul 15 2022 at 20:00)
• Groups in coq (7 messages, latest: Jul 14 2022 at 14:31)
• Haskell extraction deriving Show (10 messages, latest: Jul 14 2022 at 11:08)
• ✔ (Newbie) Tips for Systematic Organisation of Theorems (18 messages, latest: Jul 14 2022 at 07:36)
• max value (5 messages, latest: Jul 13 2022 at 18:17)
• best practice for records carrying proofs (9 messages, latest: Jul 12 2022 at 07:52)
• Documentation for cbv internals (3 messages, latest: Jul 12 2022 at 00:02)
• A Way to Define Custom Attribute? (9 messages, latest: Jul 10 2022 at 14:40)
• Lemma from library (3 messages, latest: Jul 08 2022 at 07:37)
• Using Coq platform on Mac (13 messages, latest: Jul 07 2022 at 23:41)
• Restart current sub-goal (7 messages, latest: Jul 07 2022 at 07:11)
• ✔ coq plugin (17 messages, latest: Jul 06 2022 at 06:06)
• ✔ dependent pattern matching (2 messages, latest: Jul 05 2022 at 23:51)
• Rejecting alphanumeric notations + identifier without a s... (6 messages, latest: Jul 05 2022 at 20:37)
• Function evaluation to prove type equality (6 messages, latest: Jul 04 2022 at 05:32)
• Should (custom) induction principles be transparent? (7 messages, latest: Jul 03 2022 at 11:04)
• next command? (5 messages, latest: Jul 02 2022 at 16:17)
• List formation (77 messages, latest: Jul 02 2022 at 07:31)
• unification errors (7 messages, latest: Jul 01 2022 at 11:20)
• Is wrong statement? (8 messages, latest: Jun 30 2022 at 20:25)
• Binders in theorems (18 messages, latest: Jun 30 2022 at 18:26)
• clearbody of a list of lists of identifiers (29 messages, latest: Jun 29 2022 at 14:47)
• Comparing real numbers (8 messages, latest: Jun 29 2022 at 07:42)
• Trouble with reduction (5 messages, latest: Jun 29 2022 at 07:28)
• update proof general when updating coq (1 message, latest: Jun 28 2022 at 05:33)
• Recursive functions (6 messages, latest: Jun 27 2022 at 20:18)
• A date type in coq (16 messages, latest: Jun 27 2022 at 20:16)
• Intuition for setoids? (44 messages, latest: Jun 27 2022 at 11:52)
• ✔ Error using theorem application as a Goal (21 messages, latest: Jun 27 2022 at 07:36)
• _CoqProject issues (9 messages, latest: Jun 25 2022 at 19:41)
• Notation for `Program` (3 messages, latest: Jun 25 2022 at 12:09)
• Coercion of subspaces (5 messages, latest: Jun 25 2022 at 07:43)
• ✔ CoInductive equality (5 messages, latest: Jun 25 2022 at 07:08)
• File-level Dependency Graph (21 messages, latest: Jun 24 2022 at 09:49)
• Alectryon Snippets embedded in Latex (4 messages, latest: Jun 23 2022 at 18:08)
• ✔ Difference between Two Definitions of an Indprop (13 messages, latest: Jun 23 2022 at 02:39)
• Field either real or complex (1 message, latest: Jun 22 2022 at 09:47)
• ✔ Theorem A as a Specialisation of Theorem B? (17 messages, latest: Jun 22 2022 at 08:00)
• ✔ Destruct the application of an iff theorem directly? (9 messages, latest: Jun 22 2022 at 05:57)
• ✔ Is it possible to make assert transparent? (6 messages, latest: Jun 21 2022 at 13:34)
• Are all terms inhabited? (3 messages, latest: Jun 21 2022 at 07:57)
• ✔ Destruct an enumerated datatype into FOO and not FOO? (6 messages, latest: Jun 21 2022 at 00:56)
• Nat counting (5 messages, latest: Jun 20 2022 at 14:31)
• Proof of function being injective (28 messages, latest: Jun 20 2022 at 11:31)
• Choose value based on propositions (59 messages, latest: Jun 20 2022 at 10:34)
• How to simplify obligation for Program Fixpoint (2 messages, latest: Jun 18 2022 at 17:39)
• ✔ Bind several variables before applying a lemma (8 messages, latest: Jun 18 2022 at 16:15)
• styleguide (88 messages, latest: Jun 17 2022 at 14:46)
• simple way of writing (1 message, latest: Jun 16 2022 at 18:00)
• Yet another Well_founded recursion issue (5 messages, latest: Jun 16 2022 at 16:42)
• Warning on `Variable` outside of `Section`, but not on `Cont (5 messages, latest: Jun 16 2022 at 10:24)
• ✔ Nested sigT (8 messages, latest: Jun 16 2022 at 07:18)
• Cannot find Proper instance of Parametric Morphism (5 messages, latest: Jun 15 2022 at 19:45)
• coq_makefile and tests (3 messages, latest: Jun 15 2022 at 14:13)
• Understanding &proving dependently typed Program obligation (2 messages, latest: Jun 15 2022 at 10:15)
• how to simplify (1 message, latest: Jun 14 2022 at 14:42)
• Pigeonhole principle (7 messages, latest: Jun 14 2022 at 11:34)
• Beginner's question, about `Program Fixpoint` (10 messages, latest: Jun 13 2022 at 15:28)
• Mutual recursion function in type (6 messages, latest: Jun 13 2022 at 09:17)
• ✔ Search without a module (8 messages, latest: Jun 13 2022 at 09:10)
• A simple Prop proof (6 messages, latest: Jun 13 2022 at 08:24)
• Proof of a function (5 messages, latest: Jun 13 2022 at 07:50)
• Proof mode def for mutual recursion (16 messages, latest: Jun 13 2022 at 06:20)
• Performance of `Recursive Extraction` (39 messages, latest: Jun 12 2022 at 20:34)
• Function returning sumbool (29 messages, latest: Jun 12 2022 at 08:20)
• Why parameter outside in lemmas? (7 messages, latest: Jun 12 2022 at 06:29)
• Understanding syntax (4 messages, latest: Jun 10 2022 at 19:28)
• Definition returning sumbool (13 messages, latest: Jun 10 2022 at 19:26)
• Log of type checker (3 messages, latest: Jun 10 2022 at 19:17)
• Proof Assistants Stack Exchange coordination (67 messages, latest: Jun 10 2022 at 09:30)
• compare two value (4 messages, latest: Jun 10 2022 at 06:10)
• ✔ Proof of a small scenario (13 messages, latest: Jun 10 2022 at 03:21)
• is statement true? (5 messages, latest: Jun 09 2022 at 16:48)
• Transitivity of Nat.modulo (17 messages, latest: Jun 09 2022 at 07:40)
• ✔ Prove if element (nat) is in list l, list_sum l >= element (5 messages, latest: Jun 08 2022 at 21:59)
• ✔ Prove heads of equal lists are equal (4 messages, latest: Jun 08 2022 at 19:59)
• ✔ An Extra Condition in My Induction Hypothesis? (4 messages, latest: Jun 08 2022 at 13:40)
• Formalization of Actuarial Mathematics in Coq (75 messages, latest: Jun 08 2022 at 13:39)
• Way to solve a pattern of goal (6 messages, latest: Jun 08 2022 at 07:33)
• ✔ using ALEA module (26 messages, latest: Jun 07 2022 at 19:21)
• ✔ using False = True hypothesis (5 messages, latest: Jun 07 2022 at 19:21)
• match and long identifiers (32 messages, latest: Jun 07 2022 at 14:10)
• "Not truly a recursive fixpoint" error (17 messages, latest: Jun 07 2022 at 11:41)
• Inductive types and Fixpoint (4 messages, latest: Jun 07 2022 at 09:13)
• Proving a small puzzle (24 messages, latest: Jun 07 2022 at 09:05)
• ✔ Show that (false -> Q) holds? (5 messages, latest: Jun 07 2022 at 06:28)
• What `match` tactis is useful for? (8 messages, latest: Jun 06 2022 at 20:53)
• Copying/Cloning environments for sandboxing (2 messages, latest: Jun 06 2022 at 20:17)
• ✔ Reason about head of empty list (4 messages, latest: Jun 06 2022 at 18:13)
• Searching the standard library (4 messages, latest: Jun 05 2022 at 18:53)
• Showing that a function has no fixpoint (6 messages, latest: Jun 05 2022 at 09:51)
• Proof of FS_inj in tactic mode (3 messages, latest: Jun 05 2022 at 09:26)
• Number of elements (2 messages, latest: Jun 04 2022 at 05:42)
• ✔ Build *.v Files Into a Subdirectory (13 messages, latest: Jun 02 2022 at 20:58)
• simp only (4 messages, latest: Jun 02 2022 at 19:25)
• field and powerRZ (6 messages, latest: Jun 02 2022 at 11:24)
• ✔ Define Polymorphic Datatype (8 messages, latest: Jun 02 2022 at 08:40)
• 8.15.2? (19 messages, latest: May 31 2022 at 14:53)
• on SProp (7 messages, latest: May 31 2022 at 08:27)
• ✔ Computing through opaque definitions (54 messages, latest: May 31 2022 at 07:05)
• how to prove false (5 messages, latest: May 31 2022 at 00:58)
• Design choice with setoids (16 messages, latest: May 30 2022 at 14:37)
• Notation in custom entry (22 messages, latest: May 30 2022 at 12:32)
• ✔ Unification algorithm (4 messages, latest: May 29 2022 at 15:55)
• ✔ Meaning of 'struct' (3 messages, latest: May 29 2022 at 08:25)
• Choices for axioms (16 messages, latest: May 28 2022 at 21:59)
• Higher order logic question (5 messages, latest: May 27 2022 at 22:21)
• matching of nat (2 messages, latest: May 27 2022 at 03:30)
• ✔ Creating subgoals with dependencies (4 messages, latest: May 26 2022 at 14:39)
• SSReflect and other libraries? (12 messages, latest: May 25 2022 at 20:46)
• meaning of fix (3 messages, latest: May 25 2022 at 04:02)
• how portable are .vo files? (31 messages, latest: May 24 2022 at 15:58)
• Coq as symbolic algebra or symbolic computation program (4 messages, latest: May 23 2022 at 08:31)
• Importing functions/lemmas from one Coq file to another? (50 messages, latest: May 22 2022 at 22:44)
• Unique indices in list (19 messages, latest: May 22 2022 at 20:53)
• moduls (4 messages, latest: May 22 2022 at 18:34)
• Latex and coqdoc (3 messages, latest: May 21 2022 at 21:42)
• "unpacking" Choice.sort (1 message, latest: May 21 2022 at 14:24)
• tactic for dealing with INR (4 messages, latest: May 20 2022 at 20:52)
• Building coq-library-undecidability on coq 8.12.2 (24 messages, latest: May 20 2022 at 20:08)
• Canonical name for always-true predicate (8 messages, latest: May 19 2022 at 18:25)
• Axioms Vs Inductive definitions (159 messages, latest: May 19 2022 at 15:48)
• Can opam build coqdoc while installing packages? (26 messages, latest: May 19 2022 at 01:00)
• High-level advice about formalizing mathematics (8 messages, latest: May 16 2022 at 12:44)
• Setup opam with ocaml-flambda (18 messages, latest: May 16 2022 at 09:54)
• formalization of graph coloring in Coq (11 messages, latest: May 15 2022 at 18:58)
• Code review (29 messages, latest: May 15 2022 at 07:09)
• Bridge between set theory and type theory (4 messages, latest: May 15 2022 at 02:41)
• ✔ Proof of False (6 messages, latest: May 14 2022 at 16:52)
• Gap between interactive mode and kernel? (54 messages, latest: May 14 2022 at 16:21)
• ✔ how to construct function from prop (40 messages, latest: May 14 2022 at 07:56)
• ✔ Ltac to unfold a function after a predicate (5 messages, latest: May 13 2022 at 16:57)
• `False : Prop` vs `Empty_set : Set` (4 messages, latest: May 13 2022 at 11:49)
• ✔ rewriting to isolate term (4 messages, latest: May 12 2022 at 17:41)
• Is `-async-proofs-j` broken in 8.15.1? (24 messages, latest: May 12 2022 at 09:13)
• use Gallina string with ltac's fresh (1 message, latest: May 11 2022 at 17:58)
• New to Coq (67 messages, latest: May 11 2022 at 09:33)
• print dependency graph (4 messages, latest: May 11 2022 at 07:45)
• ✔ Abstraction error in case analysis (6 messages, latest: May 11 2022 at 06:33)
• How to insert `Proof using` in all files automatically? (31 messages, latest: May 09 2022 at 18:06)
• Trying to understand behavior of destruct (66 messages, latest: May 09 2022 at 12:34)
• Make global definitions with Ltac (8 messages, latest: May 09 2022 at 12:14)
• Simplifying SSReflect Matrix (26 messages, latest: May 09 2022 at 11:01)
• ✔ Scope of unfold: specific instances and complete context (5 messages, latest: May 07 2022 at 10:43)
• ✔ Basic tactics q (6 messages, latest: May 07 2022 at 06:06)
• [OcamlAPI] [SerAPI][*] Do we have a definition in file? (4 messages, latest: May 06 2022 at 12:33)
• ✔ Factorisation of natural number (26 messages, latest: May 05 2022 at 20:43)
• Simplify the definition generated by Program Definition (7 messages, latest: May 05 2022 at 07:14)
• Group theory related theorem proving by coq. (2 messages, latest: May 04 2022 at 14:40)
• Installing coqide (56 messages, latest: May 04 2022 at 13:02)
• VsCode right pane (4 messages, latest: May 04 2022 at 10:06)
• Match on type of t - bug? (6 messages, latest: May 04 2022 at 07:50)
• Notations with default precedence (2 messages, latest: May 03 2022 at 11:13)
• problem with sudo make install (34 messages, latest: May 01 2022 at 11:06)
• How to prevent unnecessary copying? (8 messages, latest: Apr 30 2022 at 20:48)
• ✔ Stuck proving mergesort time complexity. (11 messages, latest: Apr 30 2022 at 15:47)
• Non supported pattern with ssreflect's if (3 messages, latest: Apr 30 2022 at 12:40)
• Community safety (5 messages, latest: Apr 29 2022 at 11:25)
• Proofs with forall and exists. (4 messages, latest: Apr 29 2022 at 07:25)
• ✔ Proving strong ind <-> ind. (12 messages, latest: Apr 28 2022 at 16:03)
• Does exist anything like ocp-indent or ocamlformat for Coq? (4 messages, latest: Apr 28 2022 at 14:28)
• How to define function (1 message, latest: Apr 28 2022 at 03:40)
• Unification in autosubst 2 (7 messages, latest: Apr 28 2022 at 01:18)
• ✔ Fin automation (9 messages, latest: Apr 26 2022 at 15:53)
• Pixel and its relationship (5 messages, latest: Apr 26 2022 at 12:39)
• Extraction pipeline inside and outside Coq (92 messages, latest: Apr 25 2022 at 09:21)
• ✔ Constructors with the same names (10 messages, latest: Apr 24 2022 at 14:25)
• recursive function and pattern matching (12 messages, latest: Apr 24 2022 at 12:39)
• ✔ Difficult to read universe polymorphism error (13 messages, latest: Apr 23 2022 at 13:52)
• Tactics for definitional equality (9 messages, latest: Apr 23 2022 at 09:53)
• ✔ Decidable equality (5 messages, latest: Apr 23 2022 at 02:38)
• Coq boost from 100MB L3 cache? (32 messages, latest: Apr 21 2022 at 13:38)
• ✔ Bijection between (fin n) and (fin m) implies n=m (29 messages, latest: Apr 21 2022 at 09:52)
• Having implicit arguments (2 messages, latest: Apr 21 2022 at 09:44)
• ✔ Same notation, different scope (8 messages, latest: Apr 21 2022 at 04:32)
• ✔ Mutual inductives with different parameters (46 messages, latest: Apr 20 2022 at 09:58)
• List restricted to some types (16 messages, latest: Apr 20 2022 at 09:40)
• Meaning of p: nat ? (93 messages, latest: Apr 20 2022 at 09:00)
• Properties of logic (1 message, latest: Apr 20 2022 at 07:09)
• hints on when to delete hypotheses for induction (13 messages, latest: Apr 19 2022 at 14:06)
• ✔ How to proof `In (k, v) m -> find k m = Some v` (9 messages, latest: Apr 18 2022 at 13:11)
• `Set Program Cases.` does not work as expected. (6 messages, latest: Apr 17 2022 at 17:39)
• How to overload coq notation (36 messages, latest: Apr 16 2022 at 22:23)
• ✔ Small step semantics in Coq (6 messages, latest: Apr 16 2022 at 16:41)
• solving exists statements with coq-hammer (1 message, latest: Apr 15 2022 at 02:03)
• formalizing graph coloring a la Wigderson (12 messages, latest: Apr 14 2022 at 20:49)
• stream events (2 messages, latest: Apr 14 2022 at 09:33)
• Version 6.2.3 installation (7 messages, latest: Apr 13 2022 at 08:06)
• Dependent vectors (25 messages, latest: Apr 12 2022 at 23:35)
• JMeq discriminate (5 messages, latest: Apr 12 2022 at 18:53)
• Is this some kind of refinement types (16 messages, latest: Apr 11 2022 at 14:20)
• How to change the type of a forall variable by name? (15 messages, latest: Apr 11 2022 at 10:08)
• ✔ Notation error (3 messages, latest: Apr 11 2022 at 07:27)
• Appending two hlists (3 messages, latest: Apr 11 2022 at 05:05)
• [Ltac] Tactic that "@" a function passed as argument (3 messages, latest: Apr 10 2022 at 15:51)
• ✔ Indexing into an hlist (13 messages, latest: Apr 09 2022 at 12:16)
• Proving two functions (polynomials) are same. (9 messages, latest: Apr 08 2022 at 18:13)
• What does any value inside `{| ... |}` mean? (11 messages, latest: Apr 08 2022 at 16:10)
• How to create inductively defined dependent proposition (9 messages, latest: Apr 08 2022 at 13:31)
• Coqtop help (6 messages, latest: Apr 08 2022 at 11:21)
• Multiple inputs to close box (1 message, latest: Apr 07 2022 at 18:32)
• Making proof-general / coqtop aware of .v / .vo files (why3) (3 messages, latest: Apr 06 2022 at 06:37)
• OCaml signatures in Coq (14 messages, latest: Apr 05 2022 at 19:17)
• Help getting set up with CoqIDE (5 messages, latest: Apr 05 2022 at 17:15)
• Goal display in Ltac debugger (5 messages, latest: Apr 05 2022 at 08:53)
• [ssr] congr gets stuck when given an incorrect number (14 messages, latest: Apr 04 2022 at 20:48)
• Declaring record constructor as Canonical (59 messages, latest: Apr 04 2022 at 18:05)
• Input and output relation (4 messages, latest: Apr 04 2022 at 17:40)
• Identity Coercions (23 messages, latest: Apr 02 2022 at 15:17)
• ✔ Why does this rewrite fail to work? (19 messages, latest: Mar 31 2022 at 11:41)
• Why does Hint Mode break this definition? (9 messages, latest: Mar 30 2022 at 19:59)
• Custom Entries breaking `constr` parsing (13 messages, latest: Mar 30 2022 at 13:02)
• Match on "match-with" hypothesis, regardless of type (3 messages, latest: Mar 30 2022 at 09:35)
• Repeated destruction (7 messages, latest: Mar 29 2022 at 08:55)
• 8s to set implicit arguments? (4 messages, latest: Mar 28 2022 at 06:43)
• ✔ Stuck with a proof (12 messages, latest: Mar 25 2022 at 12:13)
• Transparent and Opaque inside Ltac (3 messages, latest: Mar 25 2022 at 11:33)
• Stdpp analogue for by [] (7 messages, latest: Mar 24 2022 at 10:20)
• De-extracting back to Coq (3 messages, latest: Mar 23 2022 at 16:18)
• `:> forall {P}, ...` (26 messages, latest: Mar 22 2022 at 14:04)
• parameterized type classes vs passing functions as arguments (4 messages, latest: Mar 22 2022 at 10:56)
• Have one dimensional list (1 message, latest: Mar 21 2022 at 18:08)
• Ocaml recommended version (71 messages, latest: Mar 21 2022 at 12:18)
• Multi Sets in coq (29 messages, latest: Mar 21 2022 at 10:15)
• Universes and sigma types (66 messages, latest: Mar 19 2022 at 13:17)
• ✔ Compilation error in coq-json with coq-dev GitHub action (12 messages, latest: Mar 18 2022 at 09:05)
• Ocaml options (9 messages, latest: Mar 17 2022 at 18:05)
• Elegant way to construct proofs starting from assumptions (4 messages, latest: Mar 16 2022 at 21:23)
• Show patterns a variable could take (32 messages, latest: Mar 16 2022 at 14:57)
• Stack Exchange bot and proof assistants (10 messages, latest: Mar 16 2022 at 14:34)
• repeat function (3 messages, latest: Mar 15 2022 at 18:04)
• Error reporting (7 messages, latest: Mar 15 2022 at 14:52)
• simpl tactic from Logical Foundations: basics (3 messages, latest: Mar 14 2022 at 21:31)
• Better emacs indentation (1 message, latest: Mar 14 2022 at 20:18)
• what is unshelving ? (4 messages, latest: Mar 14 2022 at 16:56)
• Value of a subtype (23 messages, latest: Mar 14 2022 at 11:37)
• Apply refuses to be applied (9 messages, latest: Mar 09 2022 at 22:45)
• Unifying ring and field tactic with ring/field typeclass (4 messages, latest: Mar 09 2022 at 04:45)
• Equations type error on `fin t` while `Program` does not (1 message, latest: Mar 08 2022 at 16:04)
• How to use `Permutation` type? (14 messages, latest: Mar 08 2022 at 12:25)
• refman: avoiding highlighting by default? (20 messages, latest: Mar 07 2022 at 22:18)
• ✔ Automation of .v file compiling (makefile?) (17 messages, latest: Mar 07 2022 at 21:46)
• ✔ Simultaneous set/remember (5 messages, latest: Mar 07 2022 at 15:04)
• newman' s lemma and hidley rose lemma (1 message, latest: Mar 07 2022 at 08:06)
• path_indution tactic in HoTT (3 messages, latest: Mar 07 2022 at 01:53)
• ✔ Different scopes with the same delimiting key (4 messages, latest: Mar 04 2022 at 13:41)
• Tactic to change type of goal (3 messages, latest: Mar 02 2022 at 23:43)
• ✔ Primitive Projections (21 messages, latest: Mar 02 2022 at 18:15)
• ✔ Another rew lemma (6 messages, latest: Mar 02 2022 at 18:15)
• How to prove that a function is equal to a theorem (18 messages, latest: Mar 01 2022 at 20:24)
• ✔ A rew lemma (9 messages, latest: Mar 01 2022 at 16:48)
• Order of side conditions for ssr rewrite (8 messages, latest: Mar 01 2022 at 13:02)
• Where to learn about co induction (59 messages, latest: Feb 28 2022 at 20:00)
• Equations simultaneous `with` (1 message, latest: Feb 28 2022 at 16:59)
• ✔ Record type scope (17 messages, latest: Feb 28 2022 at 15:00)
• Does nat_rec from hott library compute? (6 messages, latest: Feb 28 2022 at 14:58)
• `coqc -vok` not creating `vok` files (4 messages, latest: Feb 27 2022 at 22:20)
• How to use nat in custom notations? (1 message, latest: Feb 27 2022 at 00:04)
• ✔ Stop auto scrolling on big proofs in Proof General (4 messages, latest: Feb 25 2022 at 22:42)
• η for records (7 messages, latest: Feb 24 2022 at 14:18)
• Coq community survey 2022 (2 messages, latest: Feb 21 2022 at 15:34)
• Destruct terms of indexed types (5 messages, latest: Feb 21 2022 at 01:10)
• Cant get Hint Cut to work (3 messages, latest: Feb 20 2022 at 15:52)
• proving invariance of a function under reordering lists (15 messages, latest: Feb 20 2022 at 10:17)
• ✔ Comuptation Rules for rect? (6 messages, latest: Feb 20 2022 at 09:07)
• mathcomp on platform (84 messages, latest: Feb 19 2022 at 16:21)
• proofs to learn from (8 messages, latest: Feb 19 2022 at 11:24)
• How to prove induction principle (28 messages, latest: Feb 18 2022 at 22:24)
• compiling a project (2 messages, latest: Feb 18 2022 at 21:35)
• omega (3 messages, latest: Feb 18 2022 at 21:17)
• The logic behind existential quantification (4 messages, latest: Feb 18 2022 at 09:25)
• Mutual induction question (13 messages, latest: Feb 17 2022 at 23:41)
• Confusion over hand-rolled Fin (22 messages, latest: Feb 17 2022 at 20:17)
• trouble using autosubst2 (9 messages, latest: Feb 16 2022 at 18:33)
• Trouble saving scratchpad (1 message, latest: Feb 16 2022 at 18:22)
• Coercion and Funclass (11 messages, latest: Feb 16 2022 at 10:25)
• apply with implicit arguments (1 message, latest: Feb 16 2022 at 10:18)
• Hurkens on decidable subfinite propositions? (6 messages, latest: Feb 15 2022 at 23:31)
• ✔ Non-ugly proof of forall n : nat, 1 == n -> 1 = n (14 messages, latest: Feb 15 2022 at 21:29)
• Coq's Winter 2022 Hackaton (30 messages, latest: Feb 14 2022 at 16:08)
• Elimination of sort Prop (11 messages, latest: Feb 14 2022 at 14:43)
• Identical surface form but different with Print All (3 messages, latest: Feb 14 2022 at 08:32)
• Proof by induction with n > k (12 messages, latest: Feb 14 2022 at 07:33)
• How to prove Acc for some relation? (21 messages, latest: Feb 13 2022 at 06:58)
• explicitly extracting an existential (37 messages, latest: Feb 12 2022 at 21:04)
• ✔ Tactic Like assert but Transparent (8 messages, latest: Feb 12 2022 at 20:25)
• ✔ Simple question about syntax/notation (11 messages, latest: Feb 12 2022 at 16:15)
• unsigned integer library using Cyclic? (56 messages, latest: Feb 10 2022 at 19:39)
• Coerce list Set to list Type (6 messages, latest: Feb 10 2022 at 17:58)
• ✔ Coercion of boundednat to nat (18 messages, latest: Feb 10 2022 at 17:35)
• undo exists tactics (13 messages, latest: Feb 10 2022 at 10:06)
• aac-tactics, fset automation, universes (17 messages, latest: Feb 10 2022 at 03:40)
• Lean vs Coq SE question (14 messages, latest: Feb 09 2022 at 13:51)
• multi destruct (4 messages, latest: Feb 09 2022 at 13:48)
• ✔ Troubleshooting missing Omega (14 messages, latest: Feb 09 2022 at 13:44)
• Reduce fix construct (14 messages, latest: Feb 08 2022 at 18:41)
• ✔ Error message while compiling using a Makefile.local (17 messages, latest: Feb 08 2022 at 16:18)
• lambda calculus eval in Coq (19 messages, latest: Feb 08 2022 at 09:23)
• ✔ UniMath Sigma Types Wont Bind a Family of Type (11 messages, latest: Feb 08 2022 at 00:59)
• CertiCoq processor (1 message, latest: Feb 06 2022 at 22:08)
• Extraction with dune (1 message, latest: Feb 06 2022 at 20:52)
• Match over fixpoint structure in Ltac? (31 messages, latest: Feb 05 2022 at 22:54)
• ✔ Making a decidable version of an inductive predicate (13 messages, latest: Feb 04 2022 at 22:55)
• ✔ Unbound value Char.chr when compiling extracted code: (4 messages, latest: Feb 04 2022 at 15:40)
• RFC: how to display fun/forall sequences mixed with let's (7 messages, latest: Feb 04 2022 at 12:29)
• Why lia can't prove `m <= M / n -> n * m <= M` (27 messages, latest: Feb 04 2022 at 12:09)
• Shallow embedding of modules (13 messages, latest: Feb 04 2022 at 11:16)
• Literate programming / html or latex documentation (10 messages, latest: Feb 04 2022 at 03:16)
• Parsec not importing `guard`? (10 messages, latest: Feb 03 2022 at 22:06)
• Outreachy and Google Summer of Code for Coq (41 messages, latest: Feb 03 2022 at 17:18)
• convert nat to string (2 messages, latest: Feb 01 2022 at 21:30)
• nat to digits (7 messages, latest: Feb 01 2022 at 19:55)
• ✔ Same type in multiple definitions (10 messages, latest: Feb 01 2022 at 11:57)
• type class resolution divergence with itrees (120 messages, latest: Feb 01 2022 at 09:08)
• Is there any JUnit plugin for Coq? (9 messages, latest: Feb 01 2022 at 00:47)
• ✔ Turning a recusive function into a lemma (10 messages, latest: Jan 31 2022 at 15:09)
• Dict of typeclass record (7 messages, latest: Jan 31 2022 at 03:05)
• Admitted for defintions (8 messages, latest: Jan 30 2022 at 12:07)
• Protecting goal evars (5 messages, latest: Jan 29 2022 at 03:21)
• ✔ Stuck in combine_split (7 messages, latest: Jan 28 2022 at 21:47)
• Iteratively developing definitions (4 messages, latest: Jan 28 2022 at 06:11)
• Definition in a proof (5 messages, latest: Jan 28 2022 at 01:05)
• Struggling with fold in proof (10 messages, latest: Jan 27 2022 at 21:53)
• assert vs have (107 messages, latest: Jan 27 2022 at 16:51)
• ✔ eliminate match in goal (4 messages, latest: Jan 27 2022 at 06:30)
• How to better document tactics? (1 message, latest: Jan 26 2022 at 13:18)
• ✔ Finding theorems (3 messages, latest: Jan 25 2022 at 22:27)
• ./configure -local no longer exists, what to use now? (1 message, latest: Jan 25 2022 at 20:57)
• ✔ HoTT library installation (13 messages, latest: Jan 25 2022 at 19:34)
• ✔ None <> Some a (4 messages, latest: Jan 25 2022 at 14:01)
• intermediate goal in proof (5 messages, latest: Jan 25 2022 at 09:20)
• ✔ Theorem prover vs proof assistant (7 messages, latest: Jan 25 2022 at 05:46)
• generate proofs by for loop? (11 messages, latest: Jan 24 2022 at 17:04)
• Cannot find a phyical path bound to logical path (15 messages, latest: Jan 24 2022 at 07:53)
• serapi usage: getting theorems in a project (1 message, latest: Jan 23 2022 at 13:37)
• ✔ coqtop xml protocol example (8 messages, latest: Jan 23 2022 at 13:31)
• Hypothesis statement (3 messages, latest: Jan 20 2022 at 16:50)
• Can I create alias when importing (3 messages, latest: Jan 20 2022 at 12:50)
• How to apply `Wf_Z.natlike_ind`? (4 messages, latest: Jan 20 2022 at 12:44)
• CoqPL is on Saturday, again (12 messages, latest: Jan 20 2022 at 11:21)
• ✔ meta.yml and mustache (11 messages, latest: Jan 20 2022 at 10:53)
• ITP (1 message, latest: Jan 20 2022 at 10:25)
• Where `strream` is defined? (3 messages, latest: Jan 19 2022 at 14:52)
• coq-proba (14 messages, latest: Jan 18 2022 at 22:36)
• length l (2 messages, latest: Jan 18 2022 at 17:08)
• decompose type pairs (11 messages, latest: Jan 18 2022 at 15:21)
• Notation for `list (option nat)` (17 messages, latest: Jan 18 2022 at 15:17)
• file io (12 messages, latest: Jan 18 2022 at 07:27)
• automation and proof reusability (5 messages, latest: Jan 18 2022 at 07:22)
• Naming induction hypothesis (3 messages, latest: Jan 17 2022 at 22:11)
• Merge variables with same types in hypothesis list (3 messages, latest: Jan 17 2022 at 16:03)
• list & bool (3 messages, latest: Jan 17 2022 at 14:44)
• Simplifying or unfolding within a term (3 messages, latest: Jan 17 2022 at 08:50)
• Holes vs bound variables (5 messages, latest: Jan 17 2022 at 06:41)
• modules, functor, trouble (10 messages, latest: Jan 15 2022 at 00:40)
• xor of 2 vectors of different sizes (10 messages, latest: Jan 14 2022 at 10:59)
• Ltac everywhere except inside branches of match? (1 message, latest: Jan 14 2022 at 04:02)
• Wrong inversion simplification (7 messages, latest: Jan 13 2022 at 18:37)
• Cousin of auto which changes goal when it fails (3 messages, latest: Jan 13 2022 at 18:32)
• How to use list (5 messages, latest: Jan 13 2022 at 18:15)
• options (19 messages, latest: Jan 12 2022 at 18:26)
• `-<` notation in ITrees? (4 messages, latest: Jan 12 2022 at 18:00)
• ✔ Making a custom entry (9 messages, latest: Jan 12 2022 at 15:54)
• ✔ specification of the lia tactic on non-linear problems (7 messages, latest: Jan 12 2022 at 11:18)
• Use external vars inside custom entry (11 messages, latest: Jan 12 2022 at 06:22)
• ✔ Error while creating simple notation (7 messages, latest: Jan 12 2022 at 04:20)
• using VST to verify commercial code (21 messages, latest: Jan 11 2022 at 18:28)
• Meaning of universe annotation (9 messages, latest: Jan 11 2022 at 10:33)
• ✔ Making a new notation scope (6 messages, latest: Jan 11 2022 at 08:50)
• Solving goal with exact (2 messages, latest: Jan 11 2022 at 07:49)
• Difference between Set and Type (13 messages, latest: Jan 10 2022 at 13:36)
• Proof of p -> q (63 messages, latest: Jan 10 2022 at 05:23)
• ✔ Is quote in string 'escaped'? (8 messages, latest: Jan 08 2022 at 19:15)
• Simple question about subtyping? (10 messages, latest: Jan 08 2022 at 15:47)
• error in writing (12 messages, latest: Jan 08 2022 at 08:18)
• Coercions and "_ = _ :> _" (13 messages, latest: Jan 07 2022 at 22:18)
• home-manager on nixos package management help? (1 message, latest: Jan 07 2022 at 16:13)
• Help debugging broken ltac script (86 messages, latest: Jan 07 2022 at 01:11)
• How to generate a random string for QuickChick? (3 messages, latest: Jan 06 2022 at 19:56)
• logical foundations (242 messages, latest: Jan 06 2022 at 16:51)
• ✔ exists vs exists2 (7 messages, latest: Jan 06 2022 at 16:33)
• [stdlib] Universes: arrow and flip (polymorphic or not) (10 messages, latest: Jan 06 2022 at 10:59)
• Coq repos without a license (2 messages, latest: Jan 06 2022 at 06:05)
• newline in string (7 messages, latest: Jan 06 2022 at 01:47)
• app function in list (4 messages, latest: Jan 05 2022 at 17:54)
• ✔ Stuck in bag_theorem (9 messages, latest: Jan 05 2022 at 15:50)
• ✔ Is there a way to avoid too many parenthesis? (8 messages, latest: Jan 05 2022 at 12:20)
• Good practice for constructing elements of record types (21 messages, latest: Jan 04 2022 at 20:28)
• less values (28 messages, latest: Jan 03 2022 at 17:36)
• ✔ Help with induction proof (14 messages, latest: Jan 03 2022 at 08:48)
• ✔ String representation of extended ASCII (41 messages, latest: Jan 02 2022 at 18:51)
• ✔ Definition of string notation (16 messages, latest: Jan 02 2022 at 16:47)
• getting around limitations of simple apply (6 messages, latest: Jan 02 2022 at 10:53)
• creating one hintdb that extends another (3 messages, latest: Jan 01 2022 at 18:47)
• Typed CPDT stackmachine example (5 messages, latest: Jan 01 2022 at 17:31)
• list length (13 messages, latest: Dec 31 2021 at 15:13)
• How to write statement? (2 messages, latest: Dec 31 2021 at 11:32)
• ✔ SProp: error at Qed (3 messages, latest: Dec 30 2021 at 17:13)
• ✔ Default type for a variable name (5 messages, latest: Dec 30 2021 at 17:03)
• ✔ Is it possible to generalize multiple vars in a single ... (3 messages, latest: Dec 29 2021 at 17:37)
• ✔ Understanding a rewrite with `app_assoc_reverse` (15 messages, latest: Dec 29 2021 at 17:36)
• ✔ rewrite tactic with nat argument (6 messages, latest: Dec 29 2021 at 16:50)
• Triangle (3 messages, latest: Dec 29 2021 at 14:55)
• ✔ CPDT stackmachine example proof (12 messages, latest: Dec 29 2021 at 14:04)
• ✔ Projections (6 messages, latest: Dec 29 2021 at 08:37)
• ✔ How to prove a <= b -> a <= S b? (5 messages, latest: Dec 28 2021 at 23:31)
• Import undoes `Ltac foo ::=` side effects (5 messages, latest: Dec 28 2021 at 20:47)
• ✔ Simple notation for `Vector.t bool` (3 messages, latest: Dec 26 2021 at 17:07)
• Record inside inductive types in a single expression (3 messages, latest: Dec 24 2021 at 14:33)
• Curious entry in documentation (10 messages, latest: Dec 24 2021 at 13:34)
• Emacs configuration (2 messages, latest: Dec 24 2021 at 12:54)
• Creating custom entry (3 messages, latest: Dec 23 2021 at 10:19)
• ✔ Error in typeDenote function (7 messages, latest: Dec 23 2021 at 10:03)
• Coercion source class error (11 messages, latest: Dec 22 2021 at 20:23)
• Equal to 1 (10 messages, latest: Dec 22 2021 at 18:42)
• question on paper by Coquand & Persson (14 messages, latest: Dec 22 2021 at 13:17)
• ✔ Recommended locality for type class Hint Mode (7 messages, latest: Dec 22 2021 at 08:39)
• ✔ 'Decomposed' tuple as function argument (7 messages, latest: Dec 21 2021 at 16:08)
• Unset Printing Universe and new error (4 messages, latest: Dec 21 2021 at 10:08)
• Insert all implicit arguments maximally (4 messages, latest: Dec 20 2021 at 10:16)
• contents of hint database (2 messages, latest: Dec 20 2021 at 03:57)
• pattern matching with two parameters (11 messages, latest: Dec 19 2021 at 12:57)
• seeking rewrite_strat examples (12 messages, latest: Dec 17 2021 at 09:24)
• Ltac2 in Notations (1 message, latest: Dec 16 2021 at 19:20)
• ✔ Ghost universe level with cumulative record (3 messages, latest: Dec 15 2021 at 15:23)
• seeking feature wishes for hint db modifiers (1 message, latest: Dec 15 2021 at 13:17)
• Why does my fix for a universe problem work? (2 messages, latest: Dec 14 2021 at 18:29)
• ✔ Construct a function from a point (5 messages, latest: Dec 14 2021 at 15:50)
• Alectryon in slides (52 messages, latest: Dec 10 2021 at 13:10)
• ✔ Threading context between sections (76 messages, latest: Dec 09 2021 at 22:02)
• Call for VsCoq 0.3.6 testers (1 message, latest: Dec 09 2021 at 22:01)
• ✔ Notation, Hints and Sections (6 messages, latest: Dec 09 2021 at 16:19)
• Performance of `Include` vs `Require` at large scale (26 messages, latest: Dec 08 2021 at 21:57)
• Composition of 2 functions (3 messages, latest: Dec 08 2021 at 10:35)
• Is contra statement? (2 messages, latest: Dec 08 2021 at 09:27)
• Can I force `autorewrite` to use `setoid_rewrite`? (2 messages, latest: Dec 07 2021 at 09:07)
• Tools to parse coq documents (2 messages, latest: Dec 07 2021 at 08:58)
• Converting list of types to a sum type (3 messages, latest: Dec 07 2021 at 06:03)
• Rewrite not working (3 messages, latest: Dec 07 2021 at 02:07)
• https://coq.inria.fr/documentation down? (4 messages, latest: Dec 06 2021 at 22:37)
• coq-bignums installation fails (391 messages, latest: Dec 06 2021 at 13:29)
• PSA: ARM OCaml <4.13 reports stack overflows as SIGSEGV (2 messages, latest: Dec 06 2021 at 13:28)
• Using one recursive notation from another? (6 messages, latest: Dec 05 2021 at 16:03)
• Lots of unfold, simpl (18 messages, latest: Dec 05 2021 at 15:30)
• dune cache breaks Coq 8.14(.1) (on Mac?) (27 messages, latest: Dec 04 2021 at 11:51)
• setoid_rewrite: conditional rewriting under binder (4 messages, latest: Dec 03 2021 at 19:58)
• 'Extraction' to a different language (9 messages, latest: Dec 03 2021 at 16:32)
• how termination is proved in Coq? (121 messages, latest: Dec 03 2021 at 11:07)
• ✔ turn off coercions (4 messages, latest: Dec 03 2021 at 09:29)
• Int63 fold (3 messages, latest: Dec 02 2021 at 22:48)
• Using Gallina in formal mathematics (8 messages, latest: Dec 02 2021 at 18:33)
• Hint priority in typeclasses eauto with multiple DBs (2 messages, latest: Dec 02 2021 at 16:37)
• Disadvantages to HoTT? (49 messages, latest: Dec 02 2021 at 12:41)
• ✔ Need for comma in `Arguments` command? (7 messages, latest: Dec 02 2021 at 05:32)
• Towards a CEP for improving Search (25 messages, latest: Nov 30 2021 at 21:31)
• coq-equations "not found in table: equations.fixproto" (1 message, latest: Nov 29 2021 at 23:51)
• Working in a simpler logic in Coq (4 messages, latest: Nov 29 2021 at 22:39)
• Notation printing: space control without `format` (37 messages, latest: Nov 29 2021 at 20:19)
• Using indexed types (20 messages, latest: Nov 28 2021 at 17:35)
• use Qed for Acc proofs? (155 messages, latest: Nov 28 2021 at 15:24)
• Different statements? (2 messages, latest: Nov 28 2021 at 13:58)
• [stdlib] identity vs eq (13 messages, latest: Nov 28 2021 at 09:50)
• ✔ Ensembles that live in type (29 messages, latest: Nov 28 2021 at 02:00)
• eq_rect_eq in buchberger project (14 messages, latest: Nov 27 2021 at 20:46)
• ✔ maximum of natural numbers (30 messages, latest: Nov 27 2021 at 17:54)
• ✔ Making well-formed recursion for a function (26 messages, latest: Nov 27 2021 at 06:04)
• ✔ proof for induction on nats with two base cases (4 messages, latest: Nov 27 2021 at 04:45)
• ✔ Broke proof general while updating - ideas? (4 messages, latest: Nov 26 2021 at 17:32)
• Letting coq know that 2 `Vector.t` types are same (5 messages, latest: Nov 26 2021 at 10:49)
• Advice on managing proliferation of terms (12 messages, latest: Nov 25 2021 at 21:51)
• ✔ Pattern matching on `Bcons` (19 messages, latest: Nov 25 2021 at 04:31)
• What's the best way to get list of fins (14 messages, latest: Nov 24 2021 at 20:44)
• Behavior change of 'specialize' tactic in Coq 8.14 (4 messages, latest: Nov 24 2021 at 17:23)
• Script to fix Instance locality warnings (37 messages, latest: Nov 24 2021 at 16:09)
• ✔ stdpp: map/iterate on gmap/stringmap (4 messages, latest: Nov 24 2021 at 08:20)
• ✔ Nested inductive decidable equality (11 messages, latest: Nov 24 2021 at 08:19)
• Finding min not used number in list (6 messages, latest: Nov 24 2021 at 00:27)
• stdpp: mapM more friendly to gmap ? (1 message, latest: Nov 23 2021 at 17:00)
• ✔ Alias for a tuple type (5 messages, latest: Nov 23 2021 at 16:04)
• ✔ How to prove that R is complete space? (4 messages, latest: Nov 23 2021 at 14:43)
• Set operations in coq (13 messages, latest: Nov 21 2021 at 14:04)
• Getting element from `Some` (3 messages, latest: Nov 21 2021 at 14:03)
• General equality operation in coq (7 messages, latest: Nov 21 2021 at 11:53)
• match in proof where all branches return same prop (9 messages, latest: Nov 20 2021 at 14:02)
• error message (20 messages, latest: Nov 20 2021 at 09:12)
• Using opaque and related (3 messages, latest: Nov 20 2021 at 07:42)
• ✔ log2 in coq (8 messages, latest: Nov 19 2021 at 16:35)
• Triggering reduction under a predicate. (5 messages, latest: Nov 19 2021 at 14:10)
• Exponentiation / power operator in coq (2 messages, latest: Nov 19 2021 at 13:21)
• Alternative to auto that dont restore goal when failed (2 messages, latest: Nov 19 2021 at 06:46)
• Reverse extraction? (2 messages, latest: Nov 18 2021 at 16:58)
• how was a type constructed? (26 messages, latest: Nov 17 2021 at 09:46)
• Using 'set' and similar tactics (15 messages, latest: Nov 16 2021 at 22:59)
• Any resources on writting proofs regarding `Forall` (7 messages, latest: Nov 16 2021 at 22:16)
• Make a multiargument function (14 messages, latest: Nov 16 2021 at 22:08)
• Testing with multiple OCaml versions (40 messages, latest: Nov 16 2021 at 18:15)
• Universe polymorphic definition with unbound levels (33 messages, latest: Nov 15 2021 at 16:52)
• Computing with reals and sqrt (10 messages, latest: Nov 15 2021 at 14:14)
• contra statement ? (6 messages, latest: Nov 14 2021 at 17:36)
• ✔ How to determine the level of an operator? (4 messages, latest: Nov 12 2021 at 17:46)
• Existential variable hint (35 messages, latest: Nov 11 2021 at 21:53)
• eauto shelve vs Hint extern (6 messages, latest: Nov 10 2021 at 20:34)
• false statements about list_max (2 messages, latest: Nov 10 2021 at 17:55)
• ✔ set library recommendations (8 messages, latest: Nov 10 2021 at 14:46)
• Hint databases (33 messages, latest: Nov 10 2021 at 10:32)
• error message, product vs. lambda (33 messages, latest: Nov 10 2021 at 09:49)
• ✔ How to do replace ... by (rewrite some_lemma)? (9 messages, latest: Nov 10 2021 at 03:33)
• Abstracting error (22 messages, latest: Nov 09 2021 at 21:03)
• greatest value of list (7 messages, latest: Nov 09 2021 at 17:34)
• Decimal notation in 8.14 (3 messages, latest: Nov 09 2021 at 15:12)
• Records with eta (3 messages, latest: Nov 09 2021 at 14:52)
• `Variant` (7 messages, latest: Nov 09 2021 at 08:09)
• dependent sum types in HoTT (1 message, latest: Nov 08 2021 at 20:48)
• induction & matching pattern (1 message, latest: Nov 08 2021 at 18:12)
• Why are native arrays universe polymorphic? (1 message, latest: Nov 08 2021 at 16:17)
• fset automation (7 messages, latest: Nov 08 2021 at 10:43)
• ✔ `-Q . ""` (35 messages, latest: Nov 08 2021 at 04:05)
• How to write hypothesis? (11 messages, latest: Nov 08 2021 at 03:22)
• list free of zeros (4 messages, latest: Nov 07 2021 at 22:06)
• ✔ coq vs literate coq (8 messages, latest: Nov 07 2021 at 21:38)
• `_CoqProject` -> `dune` (16 messages, latest: Nov 07 2021 at 18:56)
• Ensembles (12 messages, latest: Nov 07 2021 at 14:05)
• Ensemble image (4 messages, latest: Nov 07 2021 at 13:28)
• Bidirectionality hint, better defaults? (2 messages, latest: Nov 06 2021 at 17:19)
• `CoFixpoint`, `with` (4 messages, latest: Nov 06 2021 at 14:37)
• pycoq (11 messages, latest: Nov 05 2021 at 11:31)
• Finding an old Coq-club post on Pollack inconsistency? (51 messages, latest: Nov 04 2021 at 15:32)
• mathcomp analysis summation proof help (1 message, latest: Nov 02 2021 at 07:29)
• ✔ How to derive strong excluded middle axiom? (5 messages, latest: Oct 30 2021 at 19:58)
• Map monad state (2 messages, latest: Oct 29 2021 at 16:13)
• Setoid notation clash? (9 messages, latest: Oct 29 2021 at 10:23)
• ✔ Is there a way to make "-" opaque (ambiguity)? (12 messages, latest: Oct 29 2021 at 08:31)
• How to update coqide? (10 messages, latest: Oct 29 2021 at 07:40)
• Verifying Rust programs (20 messages, latest: Oct 28 2021 at 11:14)
• Lemmas in a Module/File (6 messages, latest: Oct 28 2021 at 09:54)
• Sum of list excluding given index (21 messages, latest: Oct 28 2021 at 09:01)
• ✔ Arbitrary function fixed points with Coinductive types (14 messages, latest: Oct 28 2021 at 05:05)
• Typeclass resolution looping, yet not searching? (51 messages, latest: Oct 27 2021 at 23:07)
• stdpp: build a map from a list of pairs (5 messages, latest: Oct 26 2021 at 11:36)
• Importing a library using NixOS (2 messages, latest: Oct 26 2021 at 04:44)
• induction on n (3 messages, latest: Oct 26 2021 at 00:59)
• Update values (2 messages, latest: Oct 26 2021 at 00:55)
• Beginner: SF question (14 messages, latest: Oct 25 2021 at 16:06)
• How can I define ODE (ordinary differential equation)? (3 messages, latest: Oct 24 2021 at 18:13)
• Termination checking rules (1 message, latest: Oct 24 2021 at 14:37)
• Flattening sequence of lists into a sequnece (10 messages, latest: Oct 24 2021 at 14:34)
• nth element in a vector (18 messages, latest: Oct 22 2021 at 18:53)
• Custom notation not printing (5 messages, latest: Oct 22 2021 at 13:13)
• Decidable inductive predicates (52 messages, latest: Oct 22 2021 at 12:32)
• Become not to be compiled by adding other definitions (5 messages, latest: Oct 22 2021 at 12:27)
• topological sorting in mathcomp (1 message, latest: Oct 22 2021 at 08:23)
• Dependent inductives (19 messages, latest: Oct 22 2021 at 07:04)
• vos/vok and link-time universe check (29 messages, latest: Oct 21 2021 at 15:37)
• Typeclass and side condition (8 messages, latest: Oct 21 2021 at 09:18)
• simplification under binders (7 messages, latest: Oct 20 2021 at 21:35)
• How to use class? (1 message, latest: Oct 20 2021 at 19:57)
• Parameterized typeclasses (10 messages, latest: Oct 20 2021 at 16:33)
• ✔ Notation arguments, quantifiers? (7 messages, latest: Oct 20 2021 at 16:11)
• class with chosen number of functions (2 messages, latest: Oct 20 2021 at 12:48)
• How to prove statement? (2 messages, latest: Oct 19 2021 at 06:40)
• opam-repository CI fail (105 messages, latest: Oct 17 2021 at 22:02)
• ✔ How to prove that Rsqrt of squared x is Rabs x? (5 messages, latest: Oct 17 2021 at 17:00)
• length finding (9 messages, latest: Oct 17 2021 at 11:13)
• ✔ Getting Nat2Z to scope (5 messages, latest: Oct 17 2021 at 08:18)
• ✔ Use Haskell-like Import syntax (7 messages, latest: Oct 15 2021 at 21:05)
• Unfolding `Opaque` (10 messages, latest: Oct 15 2021 at 19:28)
• Apply mismatched lemma, emit equality constraint/goal (5 messages, latest: Oct 15 2021 at 11:52)
• [ssreflect] create finType from unique seq (1 message, latest: Oct 14 2021 at 15:42)
• empty list (5 messages, latest: Oct 14 2021 at 04:29)
• Overriding notations (8 messages, latest: Oct 13 2021 at 14:40)
• invert IZR (2 messages, latest: Oct 13 2021 at 14:33)
• ✔ Tips on debugging rewriting with custom relations? (4 messages, latest: Oct 12 2021 at 21:32)
• bypass universe check (4 messages, latest: Oct 12 2021 at 11:05)
• Heterogenous list in coq (31 messages, latest: Oct 12 2021 at 05:20)
• ✔ One definition in module transparent / design question (19 messages, latest: Oct 10 2021 at 09:01)
• ✔ Rewrite fails (Incorrect elimination of "N.ltb_lt up 256") (18 messages, latest: Oct 10 2021 at 06:48)
• ✔ Recursive call failing on Acc (24 messages, latest: Oct 09 2021 at 09:44)
• ✔ Normalize all subterms (20 messages, latest: Oct 08 2021 at 10:09)
• How to locally fix? (2 messages, latest: Oct 07 2021 at 07:24)
• Building Coq from source (13 messages, latest: Oct 05 2021 at 22:06)
• Compare notes on coq or related research papers (3 messages, latest: Oct 05 2021 at 22:05)
• Superglobal effects and namespaces (10 messages, latest: Oct 05 2021 at 16:44)
• good way to prove existence of records containing proofs? (8 messages, latest: Oct 05 2021 at 14:00)
• `intropattern` has been renamed (4 messages, latest: Oct 05 2021 at 10:00)
• Changing version of refman without losing page (11 messages, latest: Oct 05 2021 at 09:58)
• ✔ What is Ltac2 and should I care? (76 messages, latest: Oct 05 2021 at 06:55)
• ✔ Proof monad? (81 messages, latest: Oct 04 2021 at 12:13)
• Notation for a coinductive type (5 messages, latest: Oct 02 2021 at 13:23)
• ✔ How to write tactics that accept any number of parameters? (6 messages, latest: Oct 02 2021 at 09:43)
• Is there any way to give an argument to symmetry? (23 messages, latest: Oct 01 2021 at 15:08)
• ✔ Recursive class. (20 messages, latest: Oct 01 2021 at 10:36)
• Notation conflict only when imports in a certain order (11 messages, latest: Sep 29 2021 at 20:54)
• Implement matrixes (19 messages, latest: Sep 28 2021 at 01:16)
• "Fail failing_tactic" fails to fail (11 messages, latest: Sep 27 2021 at 21:45)
• Extending `coq-haskell` to cover `Data.Functor.Adjunction` (20 messages, latest: Sep 26 2021 at 05:24)
• ✔ OCaml opam repo certificate problem (4 messages, latest: Sep 25 2021 at 14:58)
• ✔ Help with Implicit Arguments (16 messages, latest: Sep 24 2021 at 02:29)
• VScode prettify symbols (1 message, latest: Sep 22 2021 at 11:53)
• addition of numbers (4 messages, latest: Sep 22 2021 at 00:07)
• Determine correct name of argument (53 messages, latest: Sep 21 2021 at 19:46)
• Ampersand Syntax (9 messages, latest: Sep 21 2021 at 18:35)
• Strange error (with unshelve and ssreflect) (2 messages, latest: Sep 21 2021 at 10:48)
• Existence in list (3 messages, latest: Sep 21 2021 at 07:40)
• Inductive with negative types? (10 messages, latest: Sep 20 2021 at 21:26)
• Example of `Hint Transparent` and `Hint Opaque` (7 messages, latest: Sep 20 2021 at 12:32)
• Help with induction (14 messages, latest: Sep 20 2021 at 07:25)
• Less than and conjunction in coq (7 messages, latest: Sep 18 2021 at 18:22)
• Is forward declaration possible in coq? (2 messages, latest: Sep 18 2021 at 06:53)
• Namespaces (1 message, latest: Sep 17 2021 at 19:23)
• pairs and lists (4 messages, latest: Sep 16 2021 at 22:21)
• parsing, getting started, package dependencies (27 messages, latest: Sep 16 2021 at 19:50)
• How adjust fraction/decimal point points (1 message, latest: Sep 16 2021 at 18:20)
• Natural number list (4 messages, latest: Sep 16 2021 at 16:41)
• ✔ Eliminate common terms in LHS & RHS of goal (7 messages, latest: Sep 16 2021 at 16:41)
• import categories (3 messages, latest: Sep 16 2021 at 15:40)
• SMT and CIC (5 messages, latest: Sep 14 2021 at 07:42)
• Coq function not reducing (Zwf_well_founded may be culprit) (3 messages, latest: Sep 14 2021 at 06:29)
• Search library (8 messages, latest: Sep 13 2021 at 14:16)
• Proof irrelevance for Z.lt and Z.le (10 messages, latest: Sep 13 2021 at 14:15)
• Relation with Successor (3 messages, latest: Sep 12 2021 at 14:02)
• apply command? (19 messages, latest: Sep 11 2021 at 12:46)
• Auxiliary definitions during record definition? (4 messages, latest: Sep 11 2021 at 00:22)
• Working with permutations in math-comp (4 messages, latest: Sep 10 2021 at 12:53)
• anomaly interp/impargs.ml (4 messages, latest: Sep 10 2021 at 12:32)
• Print error message from failed tactic (2 messages, latest: Sep 09 2021 at 20:10)
• Stack overflow with coqc but not inside Proof General (8 messages, latest: Sep 09 2021 at 16:44)
• First Order Theory (3 messages, latest: Sep 09 2021 at 15:24)
• Show Ltac Profile's printer (3 messages, latest: Sep 09 2021 at 12:49)
• [newbie] wolf, goat and cabbage puzzle (3 messages, latest: Sep 08 2021 at 16:56)
• ✔ Dune, _CoqProject and tests (1 message, latest: Sep 08 2021 at 07:21)
• Extraction using ExtrOcamlNatBigInt (8 messages, latest: Sep 07 2021 at 22:33)
• CCorn help (4 messages, latest: Sep 06 2021 at 15:05)
• [Newbie] Error involving curly braces (11 messages, latest: Sep 06 2021 at 08:46)
• ✔ [Newbie] Coerce a list (8 messages, latest: Sep 06 2021 at 07:53)
• ✔ [ssreflect] what is going on in this view (7 messages, latest: Sep 06 2021 at 07:38)
• relation between 3 variables (18 messages, latest: Sep 04 2021 at 03:23)
• ✔ code stopped work (5 messages, latest: Sep 02 2021 at 10:02)
• Snoc lists decomposition (3 messages, latest: Sep 01 2021 at 06:57)
• ✔ Need help with "forward_while" command (Verifiable C, VST) (8 messages, latest: Aug 31 2021 at 15:14)
• Unfolding prim projections requires `beta` — intended? (5 messages, latest: Aug 30 2021 at 14:29)
• Triggering a warning during Compute (15 messages, latest: Aug 30 2021 at 13:30)
• ✔ Difficulties verifying simple C program (27 messages, latest: Aug 28 2021 at 05:58)
• presenting a language (46 messages, latest: Aug 27 2021 at 23:13)
• if, match, lambda and scopes (1 message, latest: Aug 27 2021 at 13:56)
• Ltac2 array literals (4 messages, latest: Aug 27 2021 at 10:25)
• Prove as Prop or bool? (2 messages, latest: Aug 27 2021 at 08:43)
• Lists and Multisets (4 messages, latest: Aug 26 2021 at 03:43)
• ✔ Tactic returning a proof witness and existential variables (2 messages, latest: Aug 24 2021 at 15:01)
• Records and Typeclasses (5 messages, latest: Aug 22 2021 at 17:39)
• not actual: ssreflect solve simple cases (2 messages, latest: Aug 21 2021 at 11:27)
• match goal as lambda (13 messages, latest: Aug 20 2021 at 12:34)
• Wallis' integrals and inelegance (6 messages, latest: Aug 19 2021 at 21:54)
• ✔ how to prove trivial theorem with ssreflect (6 messages, latest: Aug 19 2021 at 12:20)
• Proofs on filters (ssreflect.seq) (2 messages, latest: Aug 17 2021 at 11:19)
• Adding doc comments breaks coqc (6 messages, latest: Aug 16 2021 at 12:47)
• Writing concatenation of sized lsit function ? (6 messages, latest: Aug 16 2021 at 09:03)
• Spacemacs and company-coq (5 messages, latest: Aug 16 2021 at 08:15)
• Debugging Eval stack overflow (5 messages, latest: Aug 15 2021 at 19:58)
• building a simple topology (17 messages, latest: Aug 15 2021 at 18:38)
• maximum element of list (6 messages, latest: Aug 14 2021 at 04:26)
• Error with conj and partial application (6 messages, latest: Aug 13 2021 at 23:18)
• User-customizable simpl? (3 messages, latest: Aug 13 2021 at 23:07)
• [noob] Usage of `Vector.take` (12 messages, latest: Aug 13 2021 at 23:05)
• A 'head' function for 'Vector.t' (9 messages, latest: Aug 13 2021 at 08:03)
• ✔ Any hints? (4 messages, latest: Aug 12 2021 at 23:10)
• Function to index elements of a vector (3 messages, latest: Aug 12 2021 at 07:20)
• Modern replacement for old quote tactic/library? (1 message, latest: Aug 11 2021 at 20:55)
• selection of proper command (2 messages, latest: Aug 11 2021 at 18:08)
• ✔ Using the standard library's reflection (Bool.reflect) (11 messages, latest: Aug 10 2021 at 07:43)
• ✔ Beginner : need help on a cpdt exercise (8 messages, latest: Aug 09 2021 at 11:54)
• coqdep lax error handling (5 messages, latest: Aug 09 2021 at 11:03)
• ✔ Beginner: discriminate with variables (8 messages, latest: Aug 09 2021 at 10:35)
• Problem in lemma writing (125 messages, latest: Aug 09 2021 at 08:21)
• Differential geometry (4 messages, latest: Aug 09 2021 at 05:20)
• ✔ coq-ext-lib combining state and either monad (12 messages, latest: Aug 06 2021 at 18:09)
• Semantics of (Strategy) Opaque on primitive projections (2 messages, latest: Aug 06 2021 at 17:27)
• ✔ How to prove this? Any hints? (3 messages, latest: Aug 06 2021 at 13:29)
• external module in Coq plugin (4 messages, latest: Aug 06 2021 at 13:12)
• Semantics of About vs Print (1 message, latest: Aug 04 2021 at 10:28)
• ✔ Indexed generalized rewriting (11 messages, latest: Aug 03 2021 at 09:09)
• ✔ opam install on MacOS fails to install coq_makefile (7 messages, latest: Aug 03 2021 at 08:55)
• ANSSI and experimental SProp (39 messages, latest: Aug 02 2021 at 14:39)
• software foundations coq version? (10 messages, latest: Aug 01 2021 at 22:07)
• ✔ Asking for hints to prove a theorem (9 messages, latest: Jul 31 2021 at 19:14)
• Rewrite confusion (3 messages, latest: Jul 30 2021 at 15:33)
• reading ssreflect related books (63 messages, latest: Jul 30 2021 at 12:00)
• Trailing spaces in notation (9 messages, latest: Jul 30 2021 at 12:00)
• ✔ [Newbie] Problem with clightgen.exe (3 messages, latest: Jul 29 2021 at 15:31)
• Strange newline in printing (17 messages, latest: Jul 28 2021 at 08:10)
• ✔ interval 4.3.0 plotting failure (4 messages, latest: Jul 28 2021 at 06:19)
• snoc induction (15 messages, latest: Jul 28 2021 at 04:20)
• erewrite and ssreflect (8 messages, latest: Jul 26 2021 at 14:54)
• ✔ PDF of "Modules in type theory with generative definiti... (2 messages, latest: Jul 24 2021 at 12:06)
• ✔ Unable to install coq dev with opam (32 messages, latest: Jul 19 2021 at 12:56)
• Unexpected failure of strict positivity in a coinductive (5 messages, latest: Jul 19 2021 at 09:43)
• Definition returning a modified vector (9 messages, latest: Jul 18 2021 at 12:18)
• Proof irrelevance/accessibility/constructivity (46 messages, latest: Jul 17 2021 at 19:51)
• Typeclass functional dependency (4 messages, latest: Jul 17 2021 at 18:50)
• ✔ [Newbie] How to prove a -> (b -> a) (4 messages, latest: Jul 16 2021 at 07:36)
• ✔ [Newbie] What does % do in coq? (10 messages, latest: Jul 16 2021 at 07:36)
• ✔ Error on a simple BST definition (4 messages, latest: Jul 16 2021 at 07:33)
• congruence and specialization (6 messages, latest: Jul 14 2021 at 10:54)
• Notation introducing a binder (2 messages, latest: Jul 14 2021 at 05:58)
• ✔ Help with plugins (4 messages, latest: Jul 13 2021 at 20:28)
• Deep Induction Schemes (18 messages, latest: Jul 13 2021 at 13:36)
• From Docker with love (63 messages, latest: Jul 12 2021 at 20:57)
• Reasoning about domains of partial functions (28 messages, latest: Jul 12 2021 at 13:26)
• First Theorem Prover War (149 messages, latest: Jul 12 2021 at 13:00)
• Synthetic topology in Homotopy Type Theory for probabilistic (2 messages, latest: Jul 12 2021 at 09:08)
• [Newbie] Creating a boolean vector type (9 messages, latest: Jul 11 2021 at 11:31)
• makefile does not call coqdep (17 messages, latest: Jul 10 2021 at 17:20)
• Can't destruct or rewrite (8 messages, latest: Jul 10 2021 at 14:03)
• [noob] isSorted not working as expected (4 messages, latest: Jul 10 2021 at 10:38)
• coq-compcert install problem (1 message, latest: Jul 10 2021 at 01:19)
• "Cannot remove" warning (6 messages, latest: Jul 09 2021 at 18:54)
• windows vs WSL (1 message, latest: Jul 07 2021 at 08:07)
• Congruence for setoids (5 messages, latest: Jul 06 2021 at 16:16)
• Rewriting in vector length proof (12 messages, latest: Jul 06 2021 at 15:37)
• compile files (5 messages, latest: Jul 06 2021 at 07:43)
• Problems with some tiny function (3 messages, latest: Jul 03 2021 at 16:32)
• Associating Number notations with custom entries (4 messages, latest: Jul 02 2021 at 15:48)
• Admitted not found in environment (9 messages, latest: Jul 02 2021 at 02:02)
• installing CoqEAL (33 messages, latest: Jul 01 2021 at 18:25)
• Interpretation scope applying under a function (6 messages, latest: Jul 01 2021 at 11:52)
• Instantiating eapply existential? (12 messages, latest: Jul 01 2021 at 11:07)
• locks in mathcomp (10 messages, latest: Jul 01 2021 at 09:10)
• Move let in hypothesis to definition in context (1 message, latest: Jun 30 2021 at 21:25)
• ssreflect intropattern blowup (18 messages, latest: Jun 30 2021 at 17:56)
• intro nth variable (5 messages, latest: Jun 30 2021 at 10:14)
• Universe constraints / Require Import (6 messages, latest: Jun 29 2021 at 18:39)
• Two-sided queue (7 messages, latest: Jun 29 2021 at 12:25)
• Gallina and Vernacular definitions (36 messages, latest: Jun 29 2021 at 06:13)
• Type Classes versus Canonical Structures? (11 messages, latest: Jun 28 2021 at 06:12)
• How to package Coq? (4 messages, latest: Jun 28 2021 at 06:04)
• How do I use instances in proofs? (13 messages, latest: Jun 27 2021 at 20:52)
• Work in classical logic with Axiom of Choice (28 messages, latest: Jun 27 2021 at 12:31)
• How to attach a version to a Coq package? (3 messages, latest: Jun 27 2021 at 10:10)
• Automation and `mathcomp`. (42 messages, latest: Jun 27 2021 at 01:21)
• Can/should modules be named as reserved words? (5 messages, latest: Jun 25 2021 at 19:02)
• What to do if Coq behaves differently on different machines? (11 messages, latest: Jun 25 2021 at 07:10)
• Delayed execution of tactic (22 messages, latest: Jun 24 2021 at 17:24)
• Reliable names from inductive definitions? (27 messages, latest: Jun 24 2021 at 14:06)
• Stack overflow in Qed. (7 messages, latest: Jun 24 2021 at 08:30)
• `false: bool` → contradiction — how? (245 messages, latest: Jun 23 2021 at 20:37)
• TC failure inside Ltac `match`? (3 messages, latest: Jun 23 2021 at 07:19)
• Ring tactic using morphisms (6 messages, latest: Jun 22 2021 at 11:47)
• LEM vs decidability (105 messages, latest: Jun 22 2021 at 11:05)
• How does the `Program` stuff work? (20 messages, latest: Jun 21 2021 at 22:31)
• Coercions inside tuples (9 messages, latest: Jun 21 2021 at 13:36)
• coq-equations install error (6 messages, latest: Jun 21 2021 at 13:18)
• Proper Rewriting with Type (11 messages, latest: Jun 21 2021 at 10:54)
• What is beautiful Coq code? (17 messages, latest: Jun 21 2021 at 08:06)
• How can I print the current goal? (3 messages, latest: Jun 20 2021 at 18:16)
• `f_equal` on data constructors? (3 messages, latest: Jun 20 2021 at 16:01)
• How to put proofs inside values? (7 messages, latest: Jun 20 2021 at 14:14)
• Decidable equality and countability on Σ types? (11 messages, latest: Jun 20 2021 at 08:29)
• Standard library for polynomials? (14 messages, latest: Jun 20 2021 at 08:29)
• What do I do with Setoid equality? (14 messages, latest: Jun 19 2021 at 20:32)
• How can I disambiguate notation? (8 messages, latest: Jun 19 2021 at 13:09)
• Customize tactics used in typeclass search (27 messages, latest: Jun 18 2021 at 12:29)
• How to compute with rational numbers? (5 messages, latest: Jun 17 2021 at 15:16)
• Successor universes (5 messages, latest: Jun 17 2021 at 07:18)
• pow_pos_strict moved? (9 messages, latest: Jun 16 2021 at 22:39)
• Multi-success TC resolution from ltac? (34 messages, latest: Jun 16 2021 at 12:16)
• apply tactic for type with indices (10 messages, latest: Jun 15 2021 at 04:42)
• Add hint, name already exists (2 messages, latest: Jun 15 2021 at 04:41)
• Error: not found in table: core.JMeq.type (3 messages, latest: Jun 09 2021 at 10:29)
• [beginner] Why doesn't rewrite work here? (4 messages, latest: Jun 09 2021 at 07:18)
• `match`, `context` and creating a lambda term in Ltac (3 messages, latest: Jun 08 2021 at 15:52)
• Getting a running version of coq.8.4.6 (9 messages, latest: Jun 08 2021 at 11:43)
• double negated LEM (7 messages, latest: Jun 08 2021 at 10:33)
• gcd of list (16 messages, latest: Jun 08 2021 at 07:22)
• Warning for unused assumptions? (3 messages, latest: Jun 06 2021 at 02:26)
• Proving absence of memory leak in Verifiable C (6 messages, latest: Jun 05 2021 at 09:37)
• Setoid_rewrite: slow down between Prop and Type (10 messages, latest: Jun 03 2021 at 18:35)
• type_scope and higher order function arguments (4 messages, latest: Jun 03 2021 at 08:57)
• trace/print during runtime? (5 messages, latest: Jun 03 2021 at 07:24)
• coq-vst not found using opam (11 messages, latest: Jun 02 2021 at 15:00)
• How to use cofix. (9 messages, latest: Jun 02 2021 at 05:56)
• Check that a term is closed in Ltac (7 messages, latest: Jun 01 2021 at 09:55)
• Rewriting Limit (1 message, latest: May 31 2021 at 12:31)
• Arrays (6 messages, latest: May 28 2021 at 09:53)
• SLF anomaly (2 messages, latest: May 27 2021 at 07:20)
• Notation tutorial? (8 messages, latest: May 26 2021 at 21:34)
• Using constructor injectivity (8 messages, latest: May 26 2021 at 15:13)
• Template polymorphism and extraction (9 messages, latest: May 26 2021 at 12:46)
• [beginner] why Check (3:Set). does not work. (6 messages, latest: May 26 2021 at 12:44)
• Opaque lemmas in dependent evaluation (14 messages, latest: May 26 2021 at 07:37)
• Recursion using map (3 messages, latest: May 25 2021 at 15:55)
• Global Qed (10 messages, latest: May 21 2021 at 17:35)
• Notation with similar prefix (9 messages, latest: May 21 2021 at 11:28)
• Coqdoc with dune (1 message, latest: May 21 2021 at 05:37)
• Chaining a type-level and a term-level coercion (5 messages, latest: May 20 2021 at 12:50)
• [ssr] "Consume" the first n elements of the stack (8 messages, latest: May 20 2021 at 10:55)
• Using pattern tactic in a subterm (12 messages, latest: May 20 2021 at 02:03)
• Profiling proof script (9 messages, latest: May 19 2021 at 15:20)
• Unfolding small part of an expression (5 messages, latest: May 19 2021 at 09:22)
• Using tactic for automated proof checks of logic problems (2 messages, latest: May 19 2021 at 04:19)
• Could I set Coq to print hexadecimal integers? (10 messages, latest: May 17 2021 at 08:03)
• building tactics from `refine` (4 messages, latest: May 16 2021 at 13:41)
• Helping unification for universe-like structure (5 messages, latest: May 15 2021 at 11:27)
• Convert SSReflect `!=` to `<>`? (18 messages, latest: May 14 2021 at 13:42)
• smooth manifolds in coq (1 message, latest: May 13 2021 at 14:20)
• Proving properties of programs using the Specif sig type (19 messages, latest: May 12 2021 at 14:22)
• bbv library: defining an alignment check (3 messages, latest: May 12 2021 at 08:35)
• QuickChick - Not Checkable (3 messages, latest: May 11 2021 at 09:39)
• Showing two types are equal inside theorem definition (4 messages, latest: May 11 2021 at 08:07)
• Universe for `pattern` (7 messages, latest: May 10 2021 at 14:05)
• Formally verified javascript? (5 messages, latest: May 09 2021 at 19:49)
• Coercion to specific Funclass? (2 messages, latest: May 09 2021 at 19:20)
• Decidable types (2 messages, latest: May 08 2021 at 20:03)
• Isabelle style simplifier for Coq? (10 messages, latest: May 07 2021 at 16:46)
• Simulate #[refine] Definition (19 messages, latest: May 07 2021 at 14:22)
• Gallina: mutual fixpoint, multiple definitions (3 messages, latest: May 06 2021 at 17:35)
• n - 0 in dep. type? (2 messages, latest: May 06 2021 at 16:51)
• Showing the position of a node in tree (5 messages, latest: May 06 2021 at 09:29)
• Subst for setoids? (2 messages, latest: May 05 2021 at 12:04)
• Tail-call optimization in reduction machines (126 messages, latest: May 05 2021 at 07:39)
• Linting coq programs (1 message, latest: May 02 2021 at 19:11)
• Implementing destruct-like tactic (3 messages, latest: May 02 2021 at 07:45)
• remembering case equality in match (6 messages, latest: May 01 2021 at 13:30)
• Antipatterns (7 messages, latest: May 01 2021 at 02:39)
• Tactics: converting between semicolons and periods (3 messages, latest: Apr 30 2021 at 21:03)
• Non-deterministic tactic application? (3 messages, latest: Apr 30 2021 at 20:04)
• Type-Checking field of records (5 messages, latest: Apr 30 2021 at 19:44)
• Formalized Divide-and-conquer for Lists (1 message, latest: Apr 30 2021 at 09:02)
• Focus based on type (21 messages, latest: Apr 29 2021 at 15:42)
• Extensionality axiom based on custom equivalence relation? (21 messages, latest: Apr 28 2021 at 18:37)
• Formally verified HTTP requests (3 messages, latest: Apr 27 2021 at 09:53)
• debugging slow autorewrite (1 message, latest: Apr 27 2021 at 08:22)
• Qed. doesn't finish (3 messages, latest: Apr 26 2021 at 17:02)
• coqidetop died badly. (4 messages, latest: Apr 25 2021 at 08:16)
• Simple proof (5 messages, latest: Apr 24 2021 at 13:09)
• [Newbie] coqidetop died badly. (24 messages, latest: Apr 24 2021 at 12:19)
• Library module (9 messages, latest: Apr 23 2021 at 18:08)
• Trigger typeclass search from auto/eauto (2 messages, latest: Apr 22 2021 at 06:40)
• Weird error with induction (2 messages, latest: Apr 21 2021 at 13:56)
• Call a Ltac tactic in a vernac command? (4 messages, latest: Apr 21 2021 at 11:43)
• make auto fail if it does not solve? (7 messages, latest: Apr 21 2021 at 07:53)
• Bidirectional CIC to reduce proof term size? (16 messages, latest: Apr 20 2021 at 17:03)
• rewriting under constructor (2 messages, latest: Apr 20 2021 at 10:33)
• Consensus on division by zero (6 messages, latest: Apr 20 2021 at 07:21)
• Using Hint Extern to progress (22 messages, latest: Apr 19 2021 at 15:01)
• How to find greatest common divisor (1 message, latest: Apr 19 2021 at 11:53)
• Real numbers sum <= sum Unable to unify error (4 messages, latest: Apr 19 2021 at 08:31)
• OPAM depopts (14 messages, latest: Apr 16 2021 at 14:33)
• Unification problem with apply and convertability (12 messages, latest: Apr 15 2021 at 16:36)
• Coq-club still down? (7 messages, latest: Apr 15 2021 at 15:30)
• Mathematical Components book example problem. (5 messages, latest: Apr 15 2021 at 15:04)
• Pointers in the stdlib documentation (5 messages, latest: Apr 15 2021 at 14:44)
• Mutual induction/wiki (1 message, latest: Apr 14 2021 at 20:56)
• Index Map proof (2 messages, latest: Apr 14 2021 at 18:15)
• Match goal's patterns and notations (4 messages, latest: Apr 14 2021 at 13:05)
• Tricky nia goals (5 messages, latest: Apr 13 2021 at 15:07)
• Possible polynomial NP-complete solution (82 messages, latest: Apr 12 2021 at 19:30)
• How to prove that geom. series (with q < 1) goes to 0 (6 messages, latest: Apr 12 2021 at 19:29)
• Weird typeclass behavior (35 messages, latest: Apr 11 2021 at 20:05)
• Can't simplify goal... (5 messages, latest: Apr 11 2021 at 12:28)
• overlapping notations in different scopes (5 messages, latest: Apr 11 2021 at 11:28)
• A better type ascription syntax `foo : bar` (44 messages, latest: Apr 10 2021 at 12:57)
• Distributive facts for Prop (6 messages, latest: Apr 07 2021 at 11:04)
• Potentially superfluous universe constraints (8 messages, latest: Apr 06 2021 at 10:14)
• EqDec and Typeclasses (example for option types) (4 messages, latest: Apr 06 2021 at 09:09)
• Coq/x64 + Ocaml 4.10.2/4.12.0 (7 messages, latest: Apr 05 2021 at 21:32)
• Overhead of cbv vs. vm_compute (6 messages, latest: Apr 05 2021 at 14:00)
• CoInduction advice (6 messages, latest: Apr 04 2021 at 20:39)
• Q_ad_equiv_bd_elim (7 messages, latest: Apr 04 2021 at 10:06)
• coq_makefile build directory (3 messages, latest: Apr 04 2021 at 07:11)
• ssreflect how bool value true can became Prop? (5 messages, latest: Apr 03 2021 at 20:11)
• Do i need to use some kind of AOC (axiom of choice) here? (2 messages, latest: Apr 03 2021 at 20:08)
• Why would the kernel type checker do this ? (9 messages, latest: Apr 03 2021 at 17:26)
• Coercion to Type (7 messages, latest: Apr 02 2021 at 10:31)
• Well-founded recursion on proof? (13 messages, latest: Apr 02 2021 at 03:32)
• Good way to change the complete goal with a convertible one (16 messages, latest: Apr 01 2021 at 13:03)
• Tactic to prove equality of pairs? (3 messages, latest: Apr 01 2021 at 10:57)
• replace an element in list (3 messages, latest: Apr 01 2021 at 06:48)
• Debug printer loader file for opam Coq? (2 messages, latest: Mar 31 2021 at 18:14)
• Print a term as Coq accepts it as input (4 messages, latest: Mar 31 2021 at 11:30)
• import ssreflect eqtype from coq (7 messages, latest: Mar 31 2021 at 08:11)
• Can't infer type parameter (12 messages, latest: Mar 31 2021 at 06:18)
• floyd-warshall algorithm (7 messages, latest: Mar 30 2021 at 08:47)
• Basic universes question (3 messages, latest: Mar 29 2021 at 22:02)
• shelve_unifiable (5 messages, latest: Mar 29 2021 at 21:36)
• Question on licensing (83 messages, latest: Mar 29 2021 at 14:35)
• External type checker for Coq (2 messages, latest: Mar 27 2021 at 07:48)
• Use `auto` to generate Σ types? (11 messages, latest: Mar 26 2021 at 16:13)
• How to solve `?Goal`? (32 messages, latest: Mar 26 2021 at 16:12)
• What is `+` in `sumbool`? (4 messages, latest: Mar 26 2021 at 08:49)
• Ltac return an identifier (15 messages, latest: Mar 25 2021 at 18:43)
• Overriding reflexivity tactic (16 messages, latest: Mar 25 2021 at 16:35)
• Tactic Notation ne_ident_list (2 messages, latest: Mar 24 2021 at 22:22)
• Force notations to be Reserved (2 messages, latest: Mar 24 2021 at 17:48)
• Local Coq CI (7 messages, latest: Mar 24 2021 at 13:31)
• Trouble installing ssreflect (46 messages, latest: Mar 24 2021 at 05:05)
• Saving theorem information to external database (7 messages, latest: Mar 23 2021 at 18:49)
• Sorting out axioms (8 messages, latest: Mar 20 2021 at 19:11)
• Proof General freezes after I-search (3 messages, latest: Mar 20 2021 at 00:12)
• coqdep -dumpgraph on 8.12 (63 messages, latest: Mar 19 2021 at 17:20)
• Diagnosing slow rewrite (4 messages, latest: Mar 19 2021 at 12:01)
• Abstract and tactic-in-terms (6 messages, latest: Mar 19 2021 at 11:27)
• Hex output default for large Q (15 messages, latest: Mar 19 2021 at 10:01)
• Wildcards in Inductive definition (7 messages, latest: Mar 18 2021 at 20:53)
• inductive application (5 messages, latest: Mar 18 2021 at 16:41)
• Breaking notation strings across multiple lines (2 messages, latest: Mar 18 2021 at 12:50)
• Contributing to stdlib (2 messages, latest: Mar 18 2021 at 12:46)
• Metavariable fails to unify with return type (3 messages, latest: Mar 17 2021 at 19:15)
• Equations: "Functional induction principle could not be..." (36 messages, latest: Mar 16 2021 at 17:33)
• Inductive predicate definiton causes Anomaly (5 messages, latest: Mar 16 2021 at 15:01)
• Gitpod (3 messages, latest: Mar 15 2021 at 15:00)
• Import Variables from Section (12 messages, latest: Mar 11 2021 at 15:19)
• Notation fail with different symbols (utf8) (12 messages, latest: Mar 11 2021 at 12:27)
• Declaring & as an infix notation breaks other notations (19 messages, latest: Mar 10 2021 at 21:36)
• segfault when compiling psatz (4 messages, latest: Mar 10 2021 at 09:25)
• Installing development Coq with OPAM (22 messages, latest: Mar 09 2021 at 07:30)
• Ltac list of hypothesis (12 messages, latest: Mar 08 2021 at 09:49)
• Print Assumptions (1 message, latest: Mar 08 2021 at 09:12)
• Thinking of making a new proof editing UI (233 messages, latest: Mar 07 2021 at 20:49)
• Scope priority (7 messages, latest: Mar 06 2021 at 12:16)
• Type classes vs canonical structures vs modules (38 messages, latest: Mar 05 2021 at 18:35)
• Ltac question: `tryif` returning `constr` (8 messages, latest: Mar 05 2021 at 11:48)
• Indexed Coinductive Types (7 messages, latest: Mar 05 2021 at 08:54)
• Coq + VST (3 messages, latest: Mar 04 2021 at 13:30)
• Ltac to check if a term is existential or not (3 messages, latest: Mar 04 2021 at 10:32)
• Future-compatibility & deprecated-hint-without-locality? (4 messages, latest: Mar 03 2021 at 14:41)
• coqdoc "table of contents" (11 messages, latest: Mar 03 2021 at 11:45)
• Proof with contradiction in hypothesis (6 messages, latest: Feb 21 2021 at 08:17)
• Type Annotation - Extraction to Ocaml (1 message, latest: Feb 21 2021 at 03:42)
• dune build / fileset / netbsd (192 messages, latest: Feb 19 2021 at 19:30)
• Notations with (* *) (14 messages, latest: Feb 19 2021 at 18:07)
• Local fix and cbn (4 messages, latest: Feb 17 2021 at 15:48)
• Unfold a constant in `Program` constraints (34 messages, latest: Feb 16 2021 at 20:37)
• [non-]reversible tactics (22 messages, latest: Feb 16 2021 at 19:06)
• A question about notation format (1 message, latest: Feb 14 2021 at 15:44)
• Anaphoric macros? (2 messages, latest: Feb 13 2021 at 05:11)
• Template polymorphism + section variables? (14 messages, latest: Feb 12 2021 at 04:59)
• Clash between Ltac2 and CompCert notations (60 messages, latest: Feb 11 2021 at 13:41)
• Beginner : printing test cases used by QuickChick (1 message, latest: Feb 04 2021 at 16:29)
• Extraction to List.fold_Left (24 messages, latest: Feb 04 2021 at 16:11)
• Performance of set (x := ..) in * (3 messages, latest: Feb 04 2021 at 11:13)
• Zenodo entries (8 messages, latest: Feb 04 2021 at 10:10)
• stackoverflow in collacoq (1 message, latest: Feb 04 2021 at 08:43)
• Bug related to SProp? (8 messages, latest: Feb 02 2021 at 12:07)
• Beginner : iterator on a context in Ltac (3 messages, latest: Jan 28 2021 at 16:00)
• Proving a tautology (6 messages, latest: Jan 28 2021 at 15:44)
• Ltac2 int division / mod (2 messages, latest: Jan 27 2021 at 10:18)
• `Let` produces beta-redexes (1 message, latest: Jan 26 2021 at 14:22)
• Finding notations (3 messages, latest: Jan 23 2021 at 02:08)
• Backtracking TC search & `Hint Extern` (1 message, latest: Jan 22 2021 at 12:17)
• `cbv`,`Set Debug Cbv`, and `Hint Transparent` (6 messages, latest: Jan 21 2021 at 13:20)
• How to check the source code of CompCert (11 messages, latest: Jan 20 2021 at 10:38)
• let in with pair in Latc (beginner) (20 messages, latest: Jan 19 2021 at 15:23)
• Notation levels for abbreviation (1 message, latest: Jan 17 2021 at 18:15)
• Plans on Flatpak for Coq (+ associated libraries)? (1 message, latest: Jan 16 2021 at 13:25)
• Coq 8.13, serapi and Alectryon (1 message, latest: Jan 15 2021 at 20:08)
• psatz and coinor-csdp (8 messages, latest: Jan 15 2021 at 20:04)
• Extracting interval (4 messages, latest: Jan 15 2021 at 14:43)
• OSX users, please test (30 messages, latest: Jan 14 2021 at 19:02)
• A formal proof of Abel-Ruffini Theorem in Coq (1 message, latest: Jan 13 2021 at 17:14)
• Linux users, a snap package is available (1 message, latest: Jan 12 2021 at 09:51)
• Dependently-typed programming in Coq: Is it tolerable? (9 messages, latest: Jan 12 2021 at 04:04)
• Coq with OCaml 4.10 (17 messages, latest: Jan 11 2021 at 19:59)
• "classical tauto"? (19 messages, latest: Jan 09 2021 at 07:58)
• Warning for `Admitted`? (9 messages, latest: Jan 07 2021 at 22:49)
• Injection for dependent constructors (4 messages, latest: Jan 07 2021 at 22:49)
• Ltac newbie question about using destruct in the tactics (7 messages, latest: Jan 07 2021 at 19:17)
• "Abstraction barriers" in software foundations (22 messages, latest: Jan 07 2021 at 07:47)
• Bad interaction with notation and names (16 messages, latest: Jan 06 2021 at 16:05)
• Record variable name (2 messages, latest: Jan 06 2021 at 13:53)
• Record syntax questions (5 messages, latest: Jan 05 2021 at 21:26)
• Generalized rewrite in list fold (3 messages, latest: Jan 05 2021 at 20:29)
• Building old Coq versions (15 messages, latest: Jan 01 2021 at 18:05)
• Rewriting in Σ-types (58 messages, latest: Jan 01 2021 at 15:22)
• Ltac2 backtracking (5 messages, latest: Jan 01 2021 at 13:37)
• implicit arguments (16 messages, latest: Dec 28 2020 at 20:30)
• Rpower zero (2 messages, latest: Dec 26 2020 at 10:47)
• Controlling hypothesis name for "induction using"? (2 messages, latest: Dec 23 2020 at 17:50)
• Extracting Reals to floats (1 message, latest: Dec 23 2020 at 02:16)
• convert code version 7.4 to version 8.12.2 (3 messages, latest: Dec 22 2020 at 08:55)
• "Trial and error" miracles — discussion (3 messages, latest: Dec 18 2020 at 19:25)
• Inverse of an integer modulo prime. (3 messages, latest: Dec 18 2020 at 11:22)
• Ltac2 stability? (10 messages, latest: Dec 16 2020 at 20:52)
• Tactic fails, but not its definition (26 messages, latest: Dec 16 2020 at 14:57)
• when ltac try fails (53 messages, latest: Dec 16 2020 at 10:45)
• dune, theories composition and several package (1 message, latest: Dec 15 2020 at 17:59)
• `Set Warnings`, `Search` warnings, and STM (5 messages, latest: Dec 15 2020 at 12:54)
• Conflict between strict warnings and Search? (5 messages, latest: Dec 13 2020 at 21:10)
• Issue with setoid rewriting on Type (16 messages, latest: Dec 11 2020 at 16:42)
• sequentializing or treating differently subgoals (ltac). (16 messages, latest: Dec 11 2020 at 15:01)
• coq.inria.fr in zenodo entry (10 messages, latest: Dec 11 2020 at 14:39)
• coq autoformatter (6 messages, latest: Dec 11 2020 at 14:03)
• Simple inequality between sum of monomes (11 messages, latest: Dec 11 2020 at 13:30)
• Trouble with extraction in coq 8.12.1 (4 messages, latest: Dec 11 2020 at 03:47)
• Get the head constant of the goal (13 messages, latest: Dec 10 2020 at 20:25)
• why can't I #[export] Existing Instance (7 messages, latest: Dec 10 2020 at 12:09)
• ltac : intros followed by exists (beginner question) (13 messages, latest: Dec 10 2020 at 10:33)
• 32 bit Coq (3 messages, latest: Dec 09 2020 at 19:52)
• Force Proof using. (vos) (46 messages, latest: Dec 09 2020 at 19:47)
• Explicit universe levels turn j > i into i+1 (4 messages, latest: Dec 08 2020 at 15:25)
• ltac intros: recover the ident of the last hypothesis (16 messages, latest: Dec 08 2020 at 15:12)
• Can't get congruence error message (12 messages, latest: Dec 08 2020 at 15:02)
• Creating evars in Ltac2 (24 messages, latest: Dec 08 2020 at 14:56)
• Compute inside a ltac term (beginner's question) (12 messages, latest: Dec 08 2020 at 11:00)
• sharing module parameters (2 messages, latest: Dec 07 2020 at 21:42)
• PG slower with high res monitor? (35 messages, latest: Dec 07 2020 at 15:59)
• Match pair of terms in Ltac (beginner question) (3 messages, latest: Dec 07 2020 at 15:01)
• Installing coqidetop dev with opam (49 messages, latest: Dec 07 2020 at 11:04)
• Testing best practices (14 messages, latest: Dec 07 2020 at 04:05)
• "The following term contains unresolved implicit arguments:" (1 message, latest: Dec 06 2020 at 17:40)
• Named goals for inductive proofs (6 messages, latest: Dec 06 2020 at 17:37)
• refine in Ltac2 (10 messages, latest: Dec 06 2020 at 01:33)
• Bazel for Coq (10 messages, latest: Dec 05 2020 at 01:12)
• Printing of goal names (3 messages, latest: Dec 04 2020 at 17:17)
• naming goals based on cases (2 messages, latest: Dec 04 2020 at 15:15)
• current goal name (9 messages, latest: Dec 04 2020 at 13:36)
• warning: `grammar entry "ident" permitted "_" in addition... (7 messages, latest: Dec 04 2020 at 08:58)
• scope of definitions in sections, modules (5 messages, latest: Dec 03 2020 at 23:08)
• match goal with context succeeding with _ but failing with ? (31 messages, latest: Dec 03 2020 at 15:33)
• Usable Context ` without ! (5 messages, latest: Dec 02 2020 at 16:09)
• Is `Bind Scope` ignored by `let`? (1 message, latest: Dec 02 2020 at 15:51)
• Can unification recognize typeclass implementations? (8 messages, latest: Dec 01 2020 at 21:18)
• Parsing problem (64 messages, latest: Dec 01 2020 at 21:11)
• -Q vs -R (31 messages, latest: Dec 01 2020 at 16:49)
• Testing, but not adding, universe constraints (10 messages, latest: Nov 30 2020 at 12:56)
• CUDW (3 messages, latest: Nov 30 2020 at 09:14)
• ltac: combined fail error messages (32 messages, latest: Nov 28 2020 at 10:41)
• Using ocamldebug for plugins (9 messages, latest: Nov 26 2020 at 15:04)
• Using non-terminal in notations (4 messages, latest: Nov 26 2020 at 13:52)
• Allowing nested proof in Coq (28 messages, latest: Nov 26 2020 at 11:22)
• Error in Coq File (35 messages, latest: Nov 26 2020 at 11:05)
• MathComp 1.12.0 released (2 messages, latest: Nov 26 2020 at 11:00)
• Finding expression bounds (2 messages, latest: Nov 26 2020 at 07:58)
• GitHub actions CI with make rather than opam (12 messages, latest: Nov 25 2020 at 22:48)
• Ltac Profiling: why so much local time (29 messages, latest: Nov 25 2020 at 16:08)
• Coq 8.13 install (6 messages, latest: Nov 24 2020 at 20:22)
• Extent of "conclusion" for apply _ in (14 messages, latest: Nov 24 2020 at 17:33)
• Ltac 2 fresh (18 messages, latest: Nov 24 2020 at 17:17)
• Coq 8.12 strange magic numbers (23 messages, latest: Nov 23 2020 at 22:52)
• A variation of nth_in for lists (89 messages, latest: Nov 23 2020 at 17:22)
• How to debug diverging "Recursive Extraction " command? (2 messages, latest: Nov 23 2020 at 13:54)
• Disambiguating between vernaculars from plugins (7 messages, latest: Nov 23 2020 at 09:39)
• typeclasses eauto: restricting the use of the local context (5 messages, latest: Nov 22 2020 at 13:38)
• ltac2/ltac1 interop (35 messages, latest: Nov 21 2020 at 19:05)
• Undestanding coq statments and writing proof (3 messages, latest: Nov 21 2020 at 16:28)
• multi-goal repeat (84 messages, latest: Nov 20 2020 at 20:21)
• coqide crashes on macOS 11 (BigSur) (34 messages, latest: Nov 20 2020 at 11:31)
• Installation of Coq in VS code on Mac OS (1 message, latest: Nov 20 2020 at 11:20)
• Debugging Coq kernel code (3 messages, latest: Nov 19 2020 at 19:24)
• Order of compilation in Makefile.coq (2 messages, latest: Nov 19 2020 at 11:29)
• _CoqProject file inside our outside of theories (12 messages, latest: Nov 19 2020 at 10:48)
• Non-recursive injection (18 messages, latest: Nov 19 2020 at 10:05)
• Fast hnf relexivity proof (10 messages, latest: Nov 17 2020 at 13:14)
• Ltac profiler (6 messages, latest: Nov 16 2020 at 18:15)
• open_constr (6 messages, latest: Nov 16 2020 at 16:14)
• Fractions in Iris (9 messages, latest: Nov 16 2020 at 11:54)
• Opaque Definition from proofterm (6 messages, latest: Nov 16 2020 at 10:30)
• Coqdoc markup (2 messages, latest: Nov 15 2020 at 17:02)
• Ltac: Destruct nested pairs nicely (9 messages, latest: Nov 14 2020 at 23:11)
• Local Definition ignored by `Import`?!? (20 messages, latest: Nov 14 2020 at 11:34)
• case on an if statement inside a let (7 messages, latest: Nov 14 2020 at 00:45)
• Mutual well-founded recursion (9 messages, latest: Nov 13 2020 at 19:59)
• Bind notation argument to notation scope (11 messages, latest: Nov 13 2020 at 13:15)
• Finite Types & Finite Graphs in MathComp (1 message, latest: Nov 13 2020 at 12:08)
• nested let destructs (13 messages, latest: Nov 13 2020 at 09:00)
• Coq on macOS 11.0 Big Sur (2 messages, latest: Nov 12 2020 at 23:54)
• Subdirectories of git repos as opam repos (5 messages, latest: Nov 12 2020 at 21:32)
• Typeclass modes and instances in scope (29 messages, latest: Nov 11 2020 at 22:03)
• What does my error mean? (11 messages, latest: Nov 10 2020 at 16:00)
• rewrite against dependent types (50 messages, latest: Nov 10 2020 at 01:01)
• CoqIDE auto completion (3 messages, latest: Nov 09 2020 at 11:52)
• flocq installation error (44 messages, latest: Nov 09 2020 at 10:39)
• Qualifying definitions by parent module (3 messages, latest: Nov 09 2020 at 09:59)
• ssr views (19 messages, latest: Nov 09 2020 at 00:01)
• Debugging typeclass resolution not selecting an instance (3 messages, latest: Nov 08 2020 at 16:57)
• sf help (8 messages, latest: Nov 08 2020 at 13:48)
• Recursive function with deep pattern matching (3 messages, latest: Nov 07 2020 at 12:25)
• Unfold Coercion (2 messages, latest: Nov 06 2020 at 16:21)
• Controlling the output of Show Proof (9 messages, latest: Nov 04 2020 at 23:08)
• Hole ineligible for typeclass resolution? (5 messages, latest: Nov 04 2020 at 12:37)
• Are Local/Global deprecated? (4 messages, latest: Nov 04 2020 at 10:00)
• Set Impredicative (3 messages, latest: Nov 03 2020 at 18:14)
• Morphisms for identity and composition? (4 messages, latest: Oct 31 2020 at 20:19)
• Generalized rewriting in predicates? (31 messages, latest: Oct 31 2020 at 20:17)
• Generalized rewriting with custom 'relation' type? (15 messages, latest: Oct 31 2020 at 19:00)
• Destruct product type equality? (4 messages, latest: Oct 31 2020 at 16:54)
• Typeclass instances in sections? (6 messages, latest: Oct 31 2020 at 03:07)
• Defer unificiation until tactic? (26 messages, latest: Oct 30 2020 at 13:47)
• Inversion with different types? (kinda cursed) (25 messages, latest: Oct 30 2020 at 02:37)
• Equations in sub-expressions (1 message, latest: Oct 30 2020 at 00:55)
• Implicit arguments of polymorphic function argument (4 messages, latest: Oct 30 2020 at 00:49)
• List Subset in Coq (5 messages, latest: Oct 29 2020 at 21:34)
• Proving log_2(n!) bound for sorting (95 messages, latest: Oct 29 2020 at 17:20)
• Ltac2 tactic tutorial (3 messages, latest: Oct 29 2020 at 16:30)
• Proof in coq (2 messages, latest: Oct 29 2020 at 11:53)
• coqbot minimize (1 message, latest: Oct 27 2020 at 15:28)
• Keeping an equation in case analysis (3 messages, latest: Oct 26 2020 at 14:48)
• Tactics intro for dependently typed programmer? (19 messages, latest: Oct 25 2020 at 15:09)
• multigoal intros (9 messages, latest: Oct 25 2020 at 03:27)
• Custom induction principle for inductive proposition (23 messages, latest: Oct 24 2020 at 21:42)
• Using Coq with VScode under windows 10 (1 message, latest: Oct 24 2020 at 19:28)
• `pattern` tactic and goals with dependencies (3 messages, latest: Oct 24 2020 at 14:12)
• Record with class instances? (18 messages, latest: Oct 23 2020 at 23:27)
• ssr confusing intro pattern (8 messages, latest: Oct 23 2020 at 21:14)
• Minimze bugs without github comment? (3 messages, latest: Oct 23 2020 at 17:45)
• Opam and library for new users (31 messages, latest: Oct 23 2020 at 15:00)
• How to escape double quote in a string? (3 messages, latest: Oct 23 2020 at 14:22)
• ulep? (6 messages, latest: Oct 23 2020 at 13:42)
• How to search in Coq? (32 messages, latest: Oct 22 2020 at 19:50)
• Meta? Is it okay to ask mathy questions here? (3 messages, latest: Oct 22 2020 at 17:32)
• Coq projects broken on Windows in the wild (9 messages, latest: Oct 22 2020 at 16:05)
• How to use proof of equality? (5 messages, latest: Oct 22 2020 at 13:57)
• Compiling a library that is already installed (7 messages, latest: Oct 22 2020 at 12:11)
• Name mangling and `(e)apply ... with` (5 messages, latest: Oct 22 2020 at 11:50)
• Idiomatic same-sized lists (7 messages, latest: Oct 22 2020 at 09:09)
• Elementary proofs (2 messages, latest: Oct 21 2020 at 14:24)
• Tactic for filling in implicits? (6 messages, latest: Oct 21 2020 at 13:03)
• Injection intro patterns (106 messages, latest: Oct 21 2020 at 09:35)
• Wrong version installs (32 messages, latest: Oct 20 2020 at 05:21)
• "Proof using + with (32 messages, latest: Oct 19 2020 at 13:06)
• coq-contribs (50 messages, latest: Oct 18 2020 at 17:27)
• How to prove things about function defined using Program (7 messages, latest: Oct 18 2020 at 04:05)
• Change plicity of context in section? (1 message, latest: Oct 17 2020 at 22:46)
• Parsing JSON (5 messages, latest: Oct 17 2020 at 12:24)
• Statistics about coq-club (12 messages, latest: Oct 17 2020 at 08:50)
• Unambiguous `constructor` (1 message, latest: Oct 17 2020 at 03:01)
• simp all using Equations (10 messages, latest: Oct 16 2020 at 21:39)
• Recursive notation in terms of another? (4 messages, latest: Oct 16 2020 at 19:54)
• Opaque does not imply Typeclasses Opaque (37 messages, latest: Oct 16 2020 at 11:37)
• Compute record projections? (16 messages, latest: Oct 16 2020 at 10:22)
• Need eq to unfold? (16 messages, latest: Oct 15 2020 at 23:17)
• setup (20 messages, latest: Oct 15 2020 at 13:12)
• Interactive computation unfolding? (3 messages, latest: Oct 14 2020 at 20:48)
• Ltac matching on multiple goals (1 message, latest: Oct 14 2020 at 15:51)
• In section: declare a variable but no instance (7 messages, latest: Oct 13 2020 at 13:19)
• Notation levels (7 messages, latest: Oct 13 2020 at 13:03)
• Level of `==` notation (5 messages, latest: Oct 13 2020 at 12:55)
• Conventions around flag settings (6 messages, latest: Oct 13 2020 at 11:17)
• #[universes(template)]? (4 messages, latest: Oct 12 2020 at 20:11)
• Notation: hiding unary constructor without parentheses (4 messages, latest: Oct 12 2020 at 17:06)
• Non-terminating Admitted (50 messages, latest: Oct 12 2020 at 16:51)
• Notations for unbound variables (2 messages, latest: Oct 12 2020 at 15:20)
• Coercion from (F A) to (F B)? (7 messages, latest: Oct 11 2020 at 11:56)
• Flycheck and _coqproject? (4 messages, latest: Oct 09 2020 at 16:55)
• Ident reflection in notations? (40 messages, latest: Oct 09 2020 at 16:01)
• Implementing hierarchies of theories in modern coq (13 messages, latest: Oct 09 2020 at 12:47)
• When to use _CoqProject vs dune? (6 messages, latest: Oct 09 2020 at 09:51)
• More Coq and distributed consensus (9 messages, latest: Oct 06 2020 at 21:07)
• How do you enter in a subscript in Coq IDE? (5 messages, latest: Oct 06 2020 at 07:42)
• Circular recursive definition (33 messages, latest: Oct 05 2020 at 22:07)
• Number of unfoldings (3 messages, latest: Oct 05 2020 at 13:15)
• Install Coq master on Debian testing (26 messages, latest: Oct 02 2020 at 16:57)
• To SSReflect or to not SSReflect? (18 messages, latest: Oct 02 2020 at 11:51)
• How to use bigop results for different ranges (1 message, latest: Sep 30 2020 at 15:43)
• Lemma as predicate? (19 messages, latest: Sep 30 2020 at 12:41)
• Prevent Program Fixpoint from auto-proving obligations (4 messages, latest: Sep 27 2020 at 19:10)
• `dependent destruction` of expressions (104 messages, latest: Sep 26 2020 at 12:32)
• Slow `autorewrite` Hint Databases (43 messages, latest: Sep 26 2020 at 05:48)
• `replace` with holes (3 messages, latest: Sep 21 2020 at 16:26)
• Unification hints and canonical structures (46 messages, latest: Sep 20 2020 at 01:24)
• How to access the function listed after Drop + use include (1 message, latest: Sep 18 2020 at 09:52)
• Game theory in Coq (12 messages, latest: Sep 17 2020 at 13:22)
• hott repo is surprisingly large (14 messages, latest: Sep 16 2020 at 14:01)
• Is Include not generative? (9 messages, latest: Sep 14 2020 at 09:51)
• Linter? (9 messages, latest: Sep 12 2020 at 10:24)
• Export notation from section? (10 messages, latest: Sep 12 2020 at 09:16)
• `refine` vs `Program` (28 messages, latest: Sep 11 2020 at 18:04)
• Coming back from `Drop.` on Coq 8.11.0 (14 messages, latest: Sep 11 2020 at 14:29)
• Travis CI using NIX: large execution time (5 messages, latest: Sep 11 2020 at 11:13)
• FreeSpec vs Coq.io ? (9 messages, latest: Sep 09 2020 at 01:03)
• Template repo for program verification (5 messages, latest: Sep 08 2020 at 13:20)
• Ltac2 & Primitive Projections (1 message, latest: Sep 04 2020 at 15:12)
• How to see defined Classes? (1 message, latest: Sep 03 2020 at 13:47)
• Turn warnings into errors (21 messages, latest: Sep 03 2020 at 12:32)
• coqdoc: breaking up long toc (1 message, latest: Sep 03 2020 at 09:44)
• Anonymous submission of appendices (5 messages, latest: Sep 02 2020 at 14:30)
• Strange unification with Acc (13 messages, latest: Sep 02 2020 at 14:27)
• Is STM a dag or a tree? (15 messages, latest: Sep 02 2020 at 08:04)
• Where do I get points and vectors from? (6 messages, latest: Aug 31 2020 at 09:06)
• simplification of polynomial expressions (3 messages, latest: Aug 30 2020 at 16:51)
• How to prove a * a + a * b + b * a + b * b = a * a + 2 * a * (14 messages, latest: Aug 29 2020 at 18:25)
• mangle-names (53 messages, latest: Aug 28 2020 at 14:55)
• QuickChick - discard-friendly conjoin? (3 messages, latest: Aug 27 2020 at 08:37)
• case analysis with a hypothesis in mind (22 messages, latest: Aug 27 2020 at 05:34)
• Mtac2 stream (1 message, latest: Aug 26 2020 at 15:08)
• Liquid haskell (3 messages, latest: Aug 25 2020 at 16:32)
• Why does registering `core.eq.type` change rewrite behavior? (13 messages, latest: Aug 24 2020 at 07:03)
• Non termination with UIP (9 messages, latest: Aug 20 2020 at 15:14)
• Ltac2: Tactic definition must be a syntactical value (2 messages, latest: Aug 20 2020 at 12:51)
• Separate package for the standard library? (2 messages, latest: Aug 19 2020 at 19:54)
• Unable to install coq-8.5.3 (8 messages, latest: Aug 19 2020 at 14:21)
• Extracting to parallel computation (1 message, latest: Aug 19 2020 at 13:34)
• Structural Recursion (8 messages, latest: Aug 17 2020 at 16:08)
• Opam packaging (of Coq libs) and `dev` versions (7 messages, latest: Aug 17 2020 at 12:04)
• Integer parsing and printing (9 messages, latest: Aug 17 2020 at 10:36)
• Coq papers from FMBC '19 are out (2 messages, latest: Aug 14 2020 at 19:41)
• `rewrite_strat repeat foo` vs `repeat (rewrite_strat foo)` (3 messages, latest: Aug 14 2020 at 14:14)
• vscode coqproject (1 message, latest: Aug 14 2020 at 08:55)
• Ltac2 (34 messages, latest: Aug 12 2020 at 17:31)
• What does the `Silent` coq flag do? (4 messages, latest: Aug 11 2020 at 18:21)
• What does `-quiet` do? (3 messages, latest: Aug 11 2020 at 15:09)
• Ltac definition (7 messages, latest: Aug 11 2020 at 08:21)
• Length of a defintion (26 messages, latest: Aug 11 2020 at 08:18)
• “Running” Proofview.tactic to see if it would succeed (2 messages, latest: Aug 10 2020 at 22:43)
• Aborting typeclass resolution in an instance (12 messages, latest: Aug 10 2020 at 12:40)
• n <= m (7 messages, latest: Aug 10 2020 at 08:13)
• Setoid rewrite with non-reflexive relations (23 messages, latest: Aug 09 2020 at 20:40)
• Vector and Fin questions (3 messages, latest: Aug 09 2020 at 19:41)
• Performing computations in proofs (3 messages, latest: Aug 09 2020 at 14:26)
• Conditional branching (7 messages, latest: Aug 08 2020 at 14:49)
• Braces outside proofs (3 messages, latest: Aug 08 2020 at 09:38)
• term sequences in ltac (8 messages, latest: Aug 06 2020 at 20:54)
• Custom TC search error messages? (2 messages, latest: Aug 05 2020 at 14:21)
• Disable typeclass search for Check (2 messages, latest: Aug 05 2020 at 13:57)
• Software Foundation for Coq 8.11 (7 messages, latest: Aug 05 2020 at 09:59)
• Coinductive existence (30 messages, latest: Aug 04 2020 at 17:16)
• "Declaring arbitrary terms as hints is fragile" (5 messages, latest: Aug 04 2020 at 09:40)
• Starting Coq IDE on CentOS (7 messages, latest: Aug 04 2020 at 09:38)
• Parameter keyword in Coq modules (9 messages, latest: Aug 04 2020 at 09:19)
• in apply, discharge non-unifiable terms through equalities? (4 messages, latest: Aug 03 2020 at 12:27)
• Proof by contradiction (3 messages, latest: Aug 03 2020 at 11:47)
• Control printing? (3 messages, latest: Aug 01 2020 at 17:31)
• CoqIDE slowness on macOS (30 messages, latest: Jul 31 2020 at 08:13)
• Why must "Parameters should be syntactically the same" (1 message, latest: Jul 30 2020 at 17:52)
• Typeclass resolution without impacting the proof term (5 messages, latest: Jul 30 2020 at 15:04)
• Simple question (3 messages, latest: Jul 30 2020 at 12:29)
• Ltac1 name of changing name of unused variable breaks tactic (13 messages, latest: Jul 30 2020 at 07:12)
• sequences of try considered harmful? (14 messages, latest: Jul 28 2020 at 17:46)
• The module system (11 messages, latest: Jul 27 2020 at 14:29)
• Compiler error for Foundations of Separation Logic (8 messages, latest: Jul 26 2020 at 02:43)
• Why are there 5 files Ranalysis1 through Ranalysis5? (1 message, latest: Jul 25 2020 at 08:54)
• Getting number of goals (4 messages, latest: Jul 25 2020 at 08:33)
• Testing the macOS installer (40 messages, latest: Jul 24 2020 at 15:31)
• Trying out metacoq (1 message, latest: Jul 23 2020 at 07:11)
• dune: How to have unit tests (2 messages, latest: Jul 21 2020 at 22:46)
• prod_curry/uncurry seem named backward (14 messages, latest: Jul 21 2020 at 02:02)
• Custom primitives (1 message, latest: Jul 20 2020 at 21:30)
• Questions on Universe Polymorphism (37 messages, latest: Jul 20 2020 at 09:53)
• Question on setoid rewrite inside `if` or `match` (5 messages, latest: Jul 20 2020 at 08:02)
• Slow rewrite with evars (16 messages, latest: Jul 18 2020 at 19:24)
• Newbie proving basic lemma on nth (9 messages, latest: Jul 18 2020 at 00:14)
• Newbie question proving strictly monotonic nat list (4 messages, latest: Jul 17 2020 at 21:46)
• Libraries that are worth learning? (34 messages, latest: Jul 17 2020 at 09:14)
• Refuting exists (33 messages, latest: Jul 17 2020 at 07:10)
• newbie question (4 messages, latest: Jul 16 2020 at 10:15)
• Terminating functions on possibly-infinite data (27 messages, latest: Jul 16 2020 at 08:14)
• unit tests in Coq (5 messages, latest: Jul 15 2020 at 20:06)
• Coq project releases and Iris (104 messages, latest: Jul 15 2020 at 16:22)
• "not found in table: metacoq.bool.false" (10 messages, latest: Jul 14 2020 at 17:34)
• Interesting definition (8 messages, latest: Jul 14 2020 at 08:07)
• Multiple files in Coq IDE (4 messages, latest: Jul 14 2020 at 07:00)
• Atomic tactic and the Ltac language (3 messages, latest: Jul 08 2020 at 14:42)
• How to use finset (1 message, latest: Jul 08 2020 at 12:55)
• Performance of Require Import (7 messages, latest: Jul 07 2020 at 10:18)
• Encoding `Unifall` via boilerplate-generating plugins (1 message, latest: Jul 07 2020 at 08:54)
• dune and parallel builds (2 messages, latest: Jul 07 2020 at 08:16)
• Formally verified RPC? (1 message, latest: Jul 06 2020 at 07:17)
• module system composition (11 messages, latest: Jul 06 2020 at 01:45)
• Arguments in tactic (10 messages, latest: Jul 05 2020 at 11:57)
• Idiomatic stdpp (14 messages, latest: Jul 04 2020 at 13:38)
• Describing the relation between two tactics (4 messages, latest: Jul 04 2020 at 02:04)
• Questions on Roosterize IJCAR talk (14 messages, latest: Jul 03 2020 at 18:22)
• SF Vol5Beta Verifiable C - Dealing with if (6 messages, latest: Jul 03 2020 at 16:45)
• compiling compcert (27 messages, latest: Jul 02 2020 at 17:33)
• Defining a proof scheme when using a type constructor (4 messages, latest: Jul 01 2020 at 20:52)
• ring tactic in mathcomp (3 messages, latest: Jul 01 2020 at 08:00)
• `coqc` can find the libraries but Proof General cannot (112 messages, latest: Jul 01 2020 at 00:55)
• Code organization (8 messages, latest: Jun 29 2020 at 17:19)
• VSCoq not working (3 messages, latest: Jun 27 2020 at 03:53)
• Lax–Milgram theorem (5 messages, latest: Jun 23 2020 at 22:04)
• Beginner games for Coq (39 messages, latest: Jun 23 2020 at 17:15)
• Explanation of foundational differences of diff provers? (1 message, latest: Jun 22 2020 at 05:37)
• Counterexamples (3 messages, latest: Jun 21 2020 at 22:42)
• Software Foundations - QuickChick TImp.v - fails to find QC (9 messages, latest: Jun 21 2020 at 02:26)
• GPT-3 -> Coq (7 messages, latest: Jun 19 2020 at 21:32)
• (Bug?) Reserved Notation and Custom Entries (3 messages, latest: Jun 19 2020 at 15:04)
• Software Foundations - QuickChick Introduction.v - error (22 messages, latest: Jun 19 2020 at 14:25)
• Software Foundations - Colors.v - color_correct (24 messages, latest: Jun 19 2020 at 14:04)
• Coq MOOCs and educational content (26 messages, latest: Jun 19 2020 at 09:28)
• examples programs based on theorem proofs (2 messages, latest: Jun 19 2020 at 08:16)
• Mutual fixpoints and duplication (1 message, latest: Jun 18 2020 at 22:38)
• Organize Imports (4 messages, latest: Jun 18 2020 at 19:19)
• Universes (111 messages, latest: Jun 18 2020 at 18:33)
• Tactics for modular arithmetic (22 messages, latest: Jun 18 2020 at 15:14)
• Implicit coercions with type class constraints (5 messages, latest: Jun 17 2020 at 20:28)
• Coq use at Amazon (13 messages, latest: Jun 17 2020 at 17:54)
• Some help with Software Foundations VFA Colors.v (19 messages, latest: Jun 17 2020 at 16:17)
• vos and vok (26 messages, latest: Jun 17 2020 at 16:07)
• Resources for getting better at proofs in Coq (4 messages, latest: Jun 17 2020 at 11:54)
• Propositional logic lemma (3 messages, latest: Jun 17 2020 at 09:12)
• KerName in tactic (3 messages, latest: Jun 16 2020 at 20:55)
• Beginner question: dependent pattern matching (18 messages, latest: Jun 16 2020 at 18:25)
• Conflict between Ltac syntax and custom notation (6 messages, latest: Jun 16 2020 at 14:31)
• Coq popularity over time (8 messages, latest: Jun 15 2020 at 21:15)
• Removing notations on input / beautify (14 messages, latest: Jun 15 2020 at 12:33)
• HoTT (86 messages, latest: Jun 14 2020 at 20:08)
• Describe Coq Command Written by User (8 messages, latest: Jun 14 2020 at 08:55)
• Ltac2 pattern stuff (7 messages, latest: Jun 13 2020 at 21:34)
• Opaque Sigma Types (9 messages, latest: Jun 13 2020 at 19:31)
• opam troubles (7 messages, latest: Jun 12 2020 at 21:59)
• Elpi question (8 messages, latest: Jun 12 2020 at 14:16)
• Equations in an abstract setting (1 message, latest: Jun 12 2020 at 09:37)
• Running mystery function unknown interpretation (4 messages, latest: Jun 11 2020 at 13:48)
• Proof General eating all RAM (1 message, latest: Jun 10 2020 at 16:39)
• Nested subset type with program tactic (3 messages, latest: Jun 10 2020 at 15:30)
• Learning category theory as a programmer (1 message, latest: Jun 10 2020 at 09:40)
• notations (2 messages, latest: Jun 09 2020 at 21:27)
• MathComp 1.11.0 released (1 message, latest: Jun 09 2020 at 14:54)
• coqdoc `<<<` (2 messages, latest: Jun 09 2020 at 14:23)
• Docker image for 8.12 (20 messages, latest: Jun 07 2020 at 19:51)
• Coq 8.11.2 (23 messages, latest: Jun 07 2020 at 17:20)
• CoqHammer 1.2.1 for Coq 8.10 and 8.11 released (1 message, latest: Jun 07 2020 at 15:44)
• Extraction to Haskell (2 messages, latest: Jun 06 2020 at 12:11)
• Singleton Inductives (6 messages, latest: Jun 05 2020 at 12:01)
• Initial release of Roosterize tool for Coq lemma generation (3 messages, latest: Jun 05 2020 at 10:18)
• Confusing match (2 messages, latest: Jun 04 2020 at 22:00)
• Tactic Notation for in clause (9 messages, latest: Jun 04 2020 at 13:25)
• Generalized Rewriting & Backtracking (3 messages, latest: Jun 04 2020 at 12:38)
• Ltac1/ssr: toplevel_selector to emulate the "last" tactical? (7 messages, latest: Jun 04 2020 at 11:31)
• Ltac (7 messages, latest: Jun 03 2020 at 16:29)
• Nix CI hash error (18 messages, latest: Jun 02 2020 at 15:40)
• invalid constructor of `sum` (11 messages, latest: Jun 02 2020 at 12:53)
• John P. Pratt logic puzzle in Coq (10 messages, latest: Jun 02 2020 at 12:35)
• Describe the tactic's structure (2 messages, latest: Jun 02 2020 at 03:40)
• OCaml extraction for Reals (13 messages, latest: May 31 2020 at 08:40)
• Encoding and reasoning about FSMs (6 messages, latest: May 29 2020 at 08:04)
• My first Coq opam package (98 messages, latest: May 28 2020 at 10:24)
• "recursive-recursive" definitions (6 messages, latest: May 27 2020 at 14:25)
• Coinduction (18 messages, latest: May 26 2020 at 08:25)
• Dune complains about a missing file (1 message, latest: May 25 2020 at 20:27)
• native_compute (3 messages, latest: May 22 2020 at 02:39)
• Tracking formalizations in Coq (27 messages, latest: May 21 2020 at 11:04)
• Parsing levels (9 messages, latest: May 20 2020 at 14:00)
• About Finite Sets in coq-contribs and stdlib (28 messages, latest: May 20 2020 at 11:57)
• Psatz (2 messages, latest: May 19 2020 at 22:05)
• TacArg in ltac (14 messages, latest: May 18 2020 at 12:28)
• Extraction of (ε, δ) proofs (5 messages, latest: May 17 2020 at 18:10)
• dune support (22 messages, latest: May 17 2020 at 13:31)
• Coq Zulip archive (1 message, latest: May 16 2020 at 14:14)
• Module System (12 messages, latest: May 15 2020 at 13:55)
• low level langues formalized in Coq (2 messages, latest: May 09 2020 at 18:26)

Last updated: Jun 01 2023 at 12:01 UTC