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