|
[install] Notes on Coq and OCaml versions / configuration
|
|
16
|
347
|
April 21, 2020
|
|
Evaluate coinductive value in proof
|
|
2
|
67
|
April 19, 2020
|
|
Another simple theorem
|
|
5
|
81
|
April 19, 2020
|
|
Writing efficient decision procedures
|
|
4
|
74
|
April 18, 2020
|
|
How to approach this (seemingly) simple theorem?
|
|
8
|
129
|
April 17, 2020
|
|
Couldn't reproduce the result of an example from Intro to CIC
|
|
4
|
75
|
April 16, 2020
|
|
Restricted Inductive Type Definition
|
|
3
|
75
|
April 16, 2020
|
|
Defining addition in another integer axiomatisation
|
|
2
|
51
|
April 16, 2020
|
|
Prove antisymmetry of leq from scratch
|
|
6
|
66
|
April 15, 2020
|
|
`well_founded_induction_type` vs `Fix`
|
|
2
|
62
|
April 14, 2020
|
|
Can't compute value, having "?Goal" inside the term
|
|
5
|
50
|
April 13, 2020
|
|
Problem With Message Window Output
|
|
3
|
65
|
April 13, 2020
|
|
Goal contains fix with argument, how to progress?
|
|
3
|
59
|
April 13, 2020
|
|
Can someone help with the proof?
|
|
2
|
65
|
April 11, 2020
|
|
Is it possible to postpone a proof?
|
|
7
|
109
|
April 9, 2020
|
|
How to formalize substructures (subrings, subspaces etc.) in Coq?
|
|
2
|
71
|
April 8, 2020
|
|
Numeral Notation for `Fin.t`
|
|
5
|
80
|
April 6, 2020
|
|
Installing, for example, Math Classes library on Windows
|
|
5
|
68
|
April 6, 2020
|
|
How to define function that finds the corresponding Field?
|
|
1
|
46
|
April 6, 2020
|
|
First steps problem: simple interval overlap proof
|
|
9
|
82
|
April 4, 2020
|
|
Nested Modules and Module Types
|
|
9
|
101
|
April 4, 2020
|
|
Compilation output files
|
|
5
|
90
|
April 3, 2020
|
|
Bijections between nat and nat * nat
|
|
4
|
145
|
March 29, 2020
|
|
Mutual recursion for nested inductive types
|
|
4
|
116
|
March 28, 2020
|
|
Machine learning and hammers for Coq
|
|
18
|
1149
|
March 27, 2020
|
|
Notation substitution and identifiers
|
|
1
|
70
|
March 26, 2020
|
|
Ltac2 reference?
|
|
5
|
216
|
March 24, 2020
|
|
Looking for a clever way of stating relationships between two functions
|
|
2
|
136
|
March 23, 2020
|
|
Use notations to define an embedded language inside Coq
|
|
10
|
263
|
March 19, 2020
|
|
Change in the Constructor tactic?
|
|
2
|
72
|
March 16, 2020
|
