Reusing values from inductive relation
|
|
2
|
118
|
July 24, 2022
|
How to unset printing everything? (e.g. implicits, notations, etc)
|
|
5
|
491
|
June 25, 2021
|
Parsing Tactics via SerAPI
|
|
5
|
441
|
July 15, 2022
|
Indiscernibility of bisimilar coinductive values: can I prove it?
|
|
9
|
163
|
July 12, 2022
|
Using Coq platform on Mac
|
|
1
|
126
|
July 7, 2022
|
SProp question: What can I actually do with a (Squash P) value?
|
|
2
|
138
|
July 7, 2022
|
Setoid_rewrite failed, but succeeded when using '<-' or 'at'
|
|
3
|
168
|
June 25, 2022
|
Apply: versus apply
|
|
4
|
204
|
June 24, 2022
|
[install] Notes on OCaml versions and Coq configuration
|
|
21
|
2071
|
June 21, 2022
|
Decidable equality with Prop-carrying type
|
|
2
|
211
|
June 12, 2022
|
How to have vscode find coq?
|
|
4
|
1192
|
June 7, 2022
|
Machine learning and hammers for Coq
|
|
45
|
4315
|
June 6, 2022
|
Induction hypothesis vs. termination checker
|
|
2
|
139
|
June 5, 2022
|
Using Add Relation for Setoid equivalence of rationals
|
|
0
|
172
|
April 26, 2022
|
One weird trick to encode modal types
|
|
0
|
162
|
April 25, 2022
|
How to import Basics.v in Induction.v of LF using VS Coq extension
|
|
6
|
781
|
April 14, 2022
|
DFA In COQ
|
|
5
|
232
|
April 13, 2022
|
Functional induction with remember
|
|
2
|
274
|
April 1, 2022
|
Completely confused by a trivial SSR proof with case
|
|
3
|
206
|
March 30, 2022
|
Annoying warnings when Requiring/Importing ssreflect
|
|
4
|
197
|
March 28, 2022
|
Inductive proof automation
|
|
6
|
642
|
March 25, 2022
|
What is a hammer/atp within the logic of coq that does things like induction in coq?
|
|
1
|
174
|
March 24, 2022
|
How to state mutual/nested lemmas
|
|
8
|
424
|
March 22, 2022
|
Saerch in VSCoq
|
|
5
|
222
|
March 22, 2022
|
Stdlib documentation online?
|
|
1
|
144
|
March 20, 2022
|
More informative response to stucked proofs?
|
|
3
|
209
|
March 18, 2022
|
Indeterminate value for partial functions trick
|
|
4
|
310
|
March 14, 2022
|
Stream of non-empty lists to stream
|
|
2
|
215
|
March 11, 2022
|
Verify a intrusive linked list is memory safe with Coq
|
|
4
|
409
|
March 7, 2022
|
How to activate the messages window in vscode like the coqide has?
|
|
1
|
353
|
March 5, 2022
|