Questions tagged [notation]

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

Filter by
Sorted by
Tagged with
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 ...
Vladimir Prigodsky's user avatar
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 "...
Mike Shulman's user avatar
  • 2,882