|
Choosing between SProp and axiomatic proof irrelevance
|
|
11
|
1122
|
August 16, 2022
|
|
Is there a solution for the problematic induction hypotheses generated using eqn:H?
|
|
10
|
963
|
August 15, 2022
|
|
Print Module [Type] lacks types
|
|
0
|
457
|
August 14, 2022
|
|
Speed of Program Instance
|
|
0
|
429
|
August 12, 2022
|
|
"Correct" way to structure modules
|
|
2
|
650
|
August 9, 2022
|
|
The reference omega was not found in the current environment
|
|
2
|
984
|
August 1, 2022
|
|
Is it possible to suppose the falsity of the goal and prove False in Coq?
|
|
5
|
1274
|
July 28, 2022
|
|
Reusing values from inductive relation
|
|
2
|
519
|
July 24, 2022
|
|
How to unset printing everything? (e.g. implicits, notations, etc)
|
|
5
|
1176
|
June 25, 2021
|
|
Parsing Tactics via SerAPI
|
|
5
|
824
|
July 15, 2022
|
|
Indiscernibility of bisimilar coinductive values: can I prove it?
|
|
9
|
429
|
July 12, 2022
|
|
Using Coq platform on Mac
|
|
1
|
647
|
July 7, 2022
|
|
SProp question: What can I actually do with a (Squash P) value?
|
|
2
|
601
|
July 7, 2022
|
|
Setoid_rewrite failed, but succeeded when using '<-' or 'at'
|
|
3
|
594
|
June 25, 2022
|
|
Apply: versus apply
|
|
4
|
807
|
June 24, 2022
|
|
[install] Notes on OCaml versions and Coq configuration
|
|
21
|
3261
|
June 21, 2022
|
|
Decidable equality with Prop-carrying type
|
|
2
|
785
|
June 12, 2022
|
|
Machine learning and hammers for Coq
|
|
45
|
7243
|
June 6, 2022
|
|
Induction hypothesis vs. termination checker
|
|
2
|
502
|
June 5, 2022
|
|
One weird trick to encode modal types
|
|
0
|
544
|
April 25, 2022
|
|
DFA In COQ
|
|
5
|
760
|
April 13, 2022
|
|
Functional induction with remember
|
|
2
|
996
|
April 1, 2022
|
|
Completely confused by a trivial SSR proof with case
|
|
3
|
537
|
March 30, 2022
|
|
Annoying warnings when Requiring/Importing ssreflect
|
|
4
|
629
|
March 28, 2022
|
|
Inductive proof automation
|
|
6
|
1106
|
March 25, 2022
|
|
What is a hammer/atp within the logic of coq that does things like induction in coq?
|
|
1
|
569
|
March 24, 2022
|
|
How to state mutual/nested lemmas
|
|
8
|
1227
|
March 22, 2022
|
|
Saerch in VSCoq
|
|
5
|
757
|
March 22, 2022
|
|
Stdlib documentation online?
|
|
1
|
397
|
March 20, 2022
|
|
More informative response to stucked proofs?
|
|
3
|
555
|
March 18, 2022
|