Questions tagged [notation]
Use this tag for questions related to how proof assistants accommodate mathematical notation and symbolism.
2
questions
3
votes
0
answers
105
views
Recursive notations with forall quantifier
How can I implement a notation of the form: ∀ x ≤ y ≤ .. ≤ z ≤ t, φ in Coq?
A similar notation (but without quantifiers) appears here
...
9
votes
2
answers
178
views
Notation for indefinite integrals
The notation $\int f(x)\, dx$ for indefinite integrals is, from a theoretical syntactic perspective, a beast. As far as I can tell, this notation binds the variable $x$ in $f(x)$, finds the "...