|
Issue with syntax in tr_rev_correct
|
|
2
|
71
|
June 27, 2024
|
|
How to destruct H involving two variables
|
|
2
|
127
|
June 27, 2024
|
|
Problem with notation in CPS ceval_step extension of LF's ImpCEvalFun
|
|
2
|
120
|
May 9, 2024
|
|
How do I write a summation on Coq?
|
|
2
|
671
|
January 9, 2023
|
|
Annoying warnings when Requiring/Importing ssreflect
|
|
4
|
624
|
March 28, 2022
|
|
Notation for a coinductive type
|
|
1
|
505
|
November 4, 2021
|
|
Overload list notation
|
|
3
|
1109
|
September 27, 2021
|
|
Defining and working with trivial finite sets like {x, y, z} easily
|
|
6
|
776
|
July 8, 2021
|
|
Bug in the parser?
|
|
5
|
869
|
April 1, 2021
|
|
What determines whether a custom entry is used for printing?
|
|
5
|
1065
|
October 6, 2020
|
|
Use notation defined in module type
|
|
2
|
1097
|
May 27, 2020
|
|
Numeral Notation for `Fin.t`
|
|
4
|
1124
|
April 6, 2020
|
|
Notation substitution and identifiers
|
|
0
|
809
|
March 26, 2020
|
|
Use notations to define an embedded language inside Coq
|
|
9
|
2255
|
March 19, 2020
|