|
About the Learning category
|
|
1
|
701
|
February 12, 2019
|
|
The reference omega was not found in the current environment
|
|
2
|
44
|
August 1, 2022
|
|
Is it possible to suppose the falsity of the goal and prove False in Coq?
|
|
5
|
76
|
July 28, 2022
|
|
Reusing values from inductive relation
|
|
2
|
38
|
July 24, 2022
|
|
Print the curried version of a function (i.e. explicitly printing the functions as an explicit chain)
|
|
2
|
43
|
July 23, 2022
|
|
How to unset printing everything? (e.g. implicits, notations, etc)
|
|
5
|
339
|
June 25, 2021
|
|
Parsing Tactics via SerAPI
|
|
5
|
355
|
July 15, 2022
|
|
Indiscernibility of bisimilar coinductive values: can I prove it?
|
|
9
|
109
|
July 12, 2022
|
|
"Qed." takes a long time
|
|
4
|
86
|
July 11, 2022
|
|
Using Coq platform on Mac
|
|
1
|
39
|
July 7, 2022
|
|
SProp question: What can I actually do with a (Squash P) value?
|
|
2
|
58
|
July 7, 2022
|
|
Setoid_rewrite failed, but succeeded when using '<-' or 'at'
|
|
3
|
77
|
June 25, 2022
|
|
Apply: versus apply
|
|
4
|
83
|
June 24, 2022
|
|
[install] Notes on OCaml versions and Coq configuration
|
|
21
|
1853
|
June 21, 2022
|
|
Decidable equality with Prop-carrying type
|
|
2
|
89
|
June 12, 2022
|
|
Official place to learn how to setup Coq make files for beginner
|
|
11
|
127
|
June 11, 2022
|
|
How to have vscode find coq?
|
|
4
|
485
|
June 7, 2022
|
|
Machine learning and hammers for Coq
|
|
45
|
3744
|
June 6, 2022
|
|
Induction hypothesis vs. termination checker
|
|
2
|
79
|
June 5, 2022
|
|
Using Add Relation for Setoid equivalence of rationals
|
|
0
|
112
|
April 26, 2022
|
|
One weird trick to encode modal types
|
|
0
|
104
|
April 25, 2022
|
|
How to import Basics.v in Induction.v of LF using VS Coq extension
|
|
6
|
278
|
April 14, 2022
|
|
DFA In COQ
|
|
5
|
143
|
April 13, 2022
|
|
Functional induction with remember
|
|
2
|
159
|
April 1, 2022
|
|
Completely confused by a trivial SSR proof with case
|
|
3
|
132
|
March 30, 2022
|
|
Annoying warnings when Requiring/Importing ssreflect
|
|
4
|
112
|
March 28, 2022
|
|
Inductive proof automation
|
|
6
|
566
|
March 25, 2022
|
|
What is a hammer/atp within the logic of coq that does things like induction in coq?
|
|
1
|
110
|
March 24, 2022
|
|
How to state mutual/nested lemmas
|
|
8
|
248
|
March 22, 2022
|
|
Saerch in VSCoq
|
|
5
|
129
|
March 22, 2022
|