|
About the Learning category
|
|
1
|
722
|
February 12, 2019
|
|
Typeclasses on functions
|
|
0
|
14
|
September 23, 2022
|
|
What is unsafe about the Ltac2.Constr.Unsafe module?
|
|
2
|
57
|
September 23, 2022
|
|
Modules vs. generalized rewrite
|
|
4
|
55
|
September 19, 2022
|
|
Best way to express that a type is inhabited in a way that allows getting the habitant
|
|
1
|
58
|
September 13, 2022
|
|
Divmod equation
|
|
3
|
41
|
September 11, 2022
|
|
Defining functions in proof mode
|
|
6
|
53
|
September 9, 2022
|
|
"Qed." takes a long time
|
|
7
|
148
|
September 1, 2022
|
|
Coq and denotational semantics
|
|
1
|
57
|
August 27, 2022
|
|
Efficient algorithms using tree
|
|
6
|
78
|
August 21, 2022
|
|
Choosing between SProp and axiomatic proof irrelevance
|
|
11
|
99
|
August 16, 2022
|
|
Is there a solution for the problematic induction hypotheses generated using eqn:H?
|
|
10
|
71
|
August 15, 2022
|
|
Print Module [Type] lacks types
|
|
0
|
39
|
August 14, 2022
|
|
Speed of Program Instance
|
|
0
|
49
|
August 12, 2022
|
|
"Correct" way to structure modules
|
|
2
|
74
|
August 9, 2022
|
|
The reference omega was not found in the current environment
|
|
2
|
83
|
August 1, 2022
|
|
Is it possible to suppose the falsity of the goal and prove False in Coq?
|
|
5
|
114
|
July 28, 2022
|
|
Reusing values from inductive relation
|
|
2
|
68
|
July 24, 2022
|
|
Print the curried version of a function (i.e. explicitly printing the functions as an explicit chain)
|
|
2
|
71
|
July 23, 2022
|
|
How to unset printing everything? (e.g. implicits, notations, etc)
|
|
5
|
387
|
June 25, 2021
|
|
Parsing Tactics via SerAPI
|
|
5
|
382
|
July 15, 2022
|
|
Indiscernibility of bisimilar coinductive values: can I prove it?
|
|
9
|
128
|
July 12, 2022
|
|
Using Coq platform on Mac
|
|
1
|
61
|
July 7, 2022
|
|
SProp question: What can I actually do with a (Squash P) value?
|
|
2
|
76
|
July 7, 2022
|
|
Setoid_rewrite failed, but succeeded when using '<-' or 'at'
|
|
3
|
104
|
June 25, 2022
|
|
Apply: versus apply
|
|
4
|
124
|
June 24, 2022
|
|
[install] Notes on OCaml versions and Coq configuration
|
|
21
|
1918
|
June 21, 2022
|
|
Decidable equality with Prop-carrying type
|
|
2
|
118
|
June 12, 2022
|
|
Official place to learn how to setup Coq make files for beginner
|
|
11
|
159
|
June 11, 2022
|
|
How to have vscode find coq?
|
|
4
|
692
|
June 7, 2022
|