|
Compute 121393+121393 causes stack overflow
|
|
8
|
690
|
March 19, 2023
|
|
Coqtop Cannot Add File to Load Path
|
|
1
|
447
|
March 14, 2023
|
|
Can I achieve some specific project with Coq?
|
|
4
|
699
|
March 11, 2023
|
|
Is it possible to define a cbn-able universe cast with universe checking disabled?
|
|
9
|
473
|
March 8, 2023
|
|
Request for feedback: new convenience tactics/options for deterministic timouts & memory limits in Coq
|
|
0
|
434
|
March 8, 2023
|
|
Survey of category theory in Coq
|
|
4
|
3921
|
March 4, 2023
|
|
How to have vscode find coq?
|
|
5
|
4928
|
February 24, 2023
|
|
How to import Basics.v in Induction.v of LF using VS Coq extension
|
|
7
|
4342
|
February 24, 2023
|
|
Abstract and concrete access to a data structure
|
|
0
|
426
|
February 22, 2023
|
|
Permutation with firstn and skipn
|
|
1
|
396
|
February 11, 2023
|
|
Is there a way to redirect Coqide messages and errors to the same output?
|
|
1
|
358
|
February 2, 2023
|
|
Stuck on destructing
|
|
2
|
608
|
January 17, 2023
|
|
How do I write a summation on Coq?
|
|
2
|
686
|
January 9, 2023
|
|
Problems rewriting with type valued relations
|
|
4
|
475
|
January 7, 2023
|
|
Print the curried version of a function (i.e. explicitly printing the functions as an explicit chain)
|
|
3
|
619
|
December 20, 2022
|
|
How to install the coq 8.14 package with opam pin when it says it can't find it?
|
|
1
|
643
|
December 11, 2022
|
|
Understand the reduction behind apply
|
|
3
|
439
|
December 7, 2022
|
|
How does one print proof terms as de bruijn indices instead of random named variables in Coq?
|
|
1
|
559
|
December 6, 2022
|
|
Type (let (a, b) = ... in something a) vs. (something (let (a, b) = ... in a))
|
|
5
|
626
|
November 8, 2022
|
|
Is it possible to share binary-only libraries across OSes?
|
|
5
|
638
|
October 19, 2022
|
|
How to be good in formal verification?
|
|
3
|
1114
|
October 7, 2022
|
|
Typeclasses on functions
|
|
1
|
448
|
September 29, 2022
|
|
Generating latex from coq theorems (Coq to Latex)
|
|
1
|
1144
|
September 26, 2022
|
|
What is unsafe about the Ltac2.Constr.Unsafe module?
|
|
2
|
562
|
September 23, 2022
|
|
Modules vs. generalized rewrite
|
|
4
|
596
|
September 19, 2022
|
|
Best way to express that a type is inhabited in a way that allows getting the habitant
|
|
1
|
617
|
September 13, 2022
|
|
Divmod equation
|
|
3
|
676
|
September 11, 2022
|
|
Defining functions in proof mode
|
|
6
|
1078
|
September 9, 2022
|
|
"Qed." takes a long time
|
|
7
|
1109
|
September 1, 2022
|
|
Coq and denotational semantics
|
|
1
|
485
|
August 27, 2022
|