|
CertiuCOS2
|
|
0
|
318
|
September 25, 2023
|
|
An inductive definition failed with error "Non strictly positive occurrence..."
|
|
6
|
521
|
September 22, 2023
|
|
Trouble installing coq-core on Windows
|
|
5
|
618
|
September 14, 2023
|
|
Coqtop is not running
|
|
8
|
1000
|
September 8, 2023
|
|
Controlling Extraction of Specific Types
|
|
0
|
230
|
September 4, 2023
|
|
Failing when use "destruct" tactic to "or" hypothesis if the conclusion is sumbool
|
|
3
|
363
|
September 4, 2023
|
|
How to read this in-clause in the match construct?
|
|
4
|
323
|
September 1, 2023
|
|
Coq official website inaccessible?
|
|
2
|
305
|
August 16, 2023
|
|
Naming inconsistency in proofs using BinInt, Zorder, and its deprecation
|
|
2
|
359
|
August 10, 2023
|
|
How does one import native cyclic integers in coq?
|
|
3
|
340
|
August 2, 2023
|
|
Name proof from Next Obligation
|
|
1
|
261
|
July 26, 2023
|
|
Automated reasoning about list permutations
|
|
2
|
423
|
July 7, 2023
|
|
Can I access Coq's way of generating readable names from inside tactics?
|
|
1
|
469
|
June 20, 2023
|
|
Extraction: adding file prefix (`open …`) & suffix (e.g. function call), from Coq or dune?
|
|
1
|
430
|
June 6, 2023
|
|
Generating depth-indexed variant of an inductive
|
|
1
|
343
|
June 16, 2023
|
|
How to parse coq statements from a coq .v file the official way?
|
|
3
|
671
|
June 15, 2023
|
|
Stuck on Software Foundations Pigeonhole Principle
|
|
1
|
838
|
June 8, 2023
|
|
Official place to learn how to setup Coq make files for beginner
|
|
14
|
2940
|
May 17, 2023
|
|
Help to criate my first proof
|
|
1
|
439
|
May 12, 2023
|
|
How to do simple structural coercion
|
|
4
|
673
|
May 8, 2023
|
|
Anonymous example
|
|
1
|
384
|
May 7, 2023
|
|
CBV with pretty syntax
|
|
1
|
454
|
April 20, 2023
|
|
Trying to get a parameterized inductive type into induction
|
|
1
|
441
|
April 16, 2023
|
|
Getting List.Exists into an induction principle
|
|
2
|
503
|
April 9, 2023
|
|
Parameterizing a type system over an abstract data type with Coq's module system
|
|
1
|
422
|
April 7, 2023
|
|
Can FSets have decidable equality?
|
|
3
|
508
|
April 7, 2023
|
|
Possible lra bug
|
|
3
|
405
|
March 28, 2023
|
|
Unexpectedly accepted eapply hypothesis
|
|
5
|
445
|
March 19, 2023
|
|
Compute 121393+121393 causes stack overflow
|
|
8
|
690
|
March 19, 2023
|
|
Coqtop Cannot Add File to Load Path
|
|
1
|
444
|
March 14, 2023
|