notation
| Topic | Replies | Views | Activity | |
|---|---|---|---|---|
| Problem with Ltac2 Notation and Control.enter |
|
3 | 82 | June 9, 2026 |
| Issue with syntax in tr_rev_correct |
|
2 | 98 | June 27, 2024 |
| How to destruct H involving two variables |
|
2 | 162 | June 27, 2024 |
| Problem with notation in CPS ceval_step extension of LF's ImpCEvalFun |
|
2 | 139 | May 9, 2024 |
| How do I write a summation on Coq? |
|
2 | 710 | January 9, 2023 |
| Annoying warnings when Requiring/Importing ssreflect |
|
4 | 689 | March 28, 2022 |
| Notation for a coinductive type |
|
1 | 520 | November 4, 2021 |
| Overload list notation |
|
3 | 1152 | September 27, 2021 |
| Defining and working with trivial finite sets like {x, y, z} easily |
|
6 | 856 | July 8, 2021 |
| Bug in the parser? |
|
5 | 920 | April 1, 2021 |
| What determines whether a custom entry is used for printing? |
|
5 | 1099 | October 6, 2020 |
| Use notation defined in module type |
|
2 | 1114 | May 27, 2020 |
| Numeral Notation for `Fin.t` |
|
4 | 1159 | April 6, 2020 |
| Notation substitution and identifiers |
|
0 | 824 | March 26, 2020 |
| Use notations to define an embedded language inside Coq |
|
9 | 2333 | March 19, 2020 |