Questions tagged [notation]

Use this tag for questions related to how proof assistants accommodate mathematical notation and symbolism.

Filter by
Sorted by
Tagged with
2 votes
0 answers

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 ...
user avatar
8 votes
2 answers

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 "...
user avatar
  • 2,109