|
Tree-sitter grammar for Rocq (release 0.2.0)
|
|
0
|
61
|
August 10, 2026
|
|
Tree-sitter grammar for Rocq
|
|
0
|
127
|
July 27, 2026
|
|
Missing `stack-compiler` folder if the SF4 book
|
|
0
|
43
|
March 4, 2026
|
|
Security Foundations (new volume of Software Foundations)
|
|
0
|
68
|
January 8, 2026
|
|
How to think of inductive types?
|
|
4
|
188
|
June 6, 2025
|
|
Why are tactics like `simpl` valid?
|
|
10
|
298
|
June 2, 2025
|
|
-beginner- recursive definition ill-formed
|
|
5
|
254
|
August 24, 2024
|
|
Showing falsity in a 'le' exercise from 'IndProp'
|
|
2
|
97
|
August 22, 2024
|
|
Issue with importing definitions from previous chapter in CoqIDE
|
|
24
|
801
|
July 10, 2024
|
|
Unable to understand the 'total_relation' question
|
|
6
|
153
|
July 3, 2024
|
|
Unable to use the induction hypothesis in In_map_iff
|
|
3
|
129
|
July 1, 2024
|
|
Unable to correctly use the 'apply' tactic
|
|
3
|
132
|
June 28, 2024
|
|
Issue with syntax in tr_rev_correct
|
|
2
|
105
|
June 27, 2024
|
|
How to destruct H involving two variables
|
|
2
|
168
|
June 27, 2024
|
|
How to prove a function is uniquely specified?
|
|
3
|
145
|
June 21, 2024
|
|
Using Coq to prove Lagrange's Theorem
|
|
1
|
178
|
May 12, 2024
|
|
Problem with notation in CPS ceval_step extension of LF's ImpCEvalFun
|
|
2
|
142
|
May 9, 2024
|
|
How to simplify single-branch match expressions?
|
|
2
|
425
|
April 8, 2024
|
|
The Lemma body_push in Verif_stack of VC
|
|
3
|
265
|
December 15, 2023
|
|
About 'syntax error: lexer: undefined token' at the beginning
|
|
2
|
791
|
October 20, 2023
|
|
How to import Basics.v in Induction.v of LF using VS Coq extension
|
|
7
|
4430
|
February 24, 2023
|
|
The reference omega was not found in the current environment
|
|
2
|
1006
|
August 1, 2022
|
|
How to use tactic forward_if Q?
|
|
4
|
853
|
September 16, 2021
|
|
How to prove this self-defined Bag Theorem?
|
|
5
|
1436
|
August 8, 2021
|
|
Extraction - System error
|
|
8
|
976
|
July 30, 2021
|
|
Software Foundations: minustwo not found in Poly.v
|
|
6
|
818
|
July 28, 2021
|
|
Software Foundations: Normalization Function Exercise
|
|
2
|
1627
|
July 26, 2021
|
|
Coq Prove code security
|
|
1
|
762
|
July 26, 2021
|
|
Software foundations: stuck at exercise `binary_inverse` in the Induction chapter
|
|
2
|
977
|
July 6, 2021
|
|
Tree Calculus
|
|
0
|
1676
|
October 14, 2020
|