|
Can I access Coq's way of generating readable names from inside tactics?
|
|
1
|
450
|
June 20, 2023
|
|
Extraction: adding file prefix (`open …`) & suffix (e.g. function call), from Coq or dune?
|
|
1
|
409
|
June 6, 2023
|
|
Generating depth-indexed variant of an inductive
|
|
1
|
329
|
June 16, 2023
|
|
How to parse coq statements from a coq .v file the official way?
|
|
3
|
624
|
June 15, 2023
|
|
Stuck on Software Foundations Pigeonhole Principle
|
|
1
|
743
|
June 8, 2023
|
|
Official place to learn how to setup Coq make files for beginner
|
|
14
|
2761
|
May 17, 2023
|
|
Help to criate my first proof
|
|
1
|
420
|
May 12, 2023
|
|
How to do simple structural coercion
|
|
4
|
631
|
May 8, 2023
|
|
Anonymous example
|
|
1
|
353
|
May 7, 2023
|
|
CBV with pretty syntax
|
|
1
|
432
|
April 20, 2023
|
|
Trying to get a parameterized inductive type into induction
|
|
1
|
423
|
April 16, 2023
|
|
Getting List.Exists into an induction principle
|
|
2
|
448
|
April 9, 2023
|
|
Parameterizing a type system over an abstract data type with Coq's module system
|
|
1
|
390
|
April 7, 2023
|
|
Can FSets have decidable equality?
|
|
3
|
481
|
April 7, 2023
|
|
Possible lra bug
|
|
3
|
389
|
March 28, 2023
|
|
Unexpectedly accepted eapply hypothesis
|
|
5
|
417
|
March 19, 2023
|
|
Compute 121393+121393 causes stack overflow
|
|
8
|
651
|
March 19, 2023
|
|
Coqtop Cannot Add File to Load Path
|
|
1
|
434
|
March 14, 2023
|
|
Can I achieve some specific project with Coq?
|
|
4
|
661
|
March 11, 2023
|
|
Is it possible to define a cbn-able universe cast with universe checking disabled?
|
|
9
|
413
|
March 8, 2023
|
|
Request for feedback: new convenience tactics/options for deterministic timouts & memory limits in Coq
|
|
0
|
407
|
March 8, 2023
|
|
Survey of category theory in Coq
|
|
4
|
3825
|
March 4, 2023
|
|
How to have vscode find coq?
|
|
5
|
4650
|
February 24, 2023
|
|
How to import Basics.v in Induction.v of LF using VS Coq extension
|
|
7
|
4016
|
February 24, 2023
|
|
Abstract and concrete access to a data structure
|
|
0
|
401
|
February 22, 2023
|
|
Permutation with firstn and skipn
|
|
1
|
380
|
February 11, 2023
|
|
Is there a way to redirect Coqide messages and errors to the same output?
|
|
1
|
352
|
February 2, 2023
|
|
Stuck on destructing
|
|
2
|
570
|
January 17, 2023
|
|
How do I write a summation on Coq?
|
|
2
|
650
|
January 9, 2023
|
|
Problems rewriting with type valued relations
|
|
4
|
452
|
January 7, 2023
|