Skip to main content

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

Factoring custom grammar rules for integers and lists in Coq custom entries

Is there a nice way to use custom entries to parse the following grammar? ("nice" meaning ~ "without massive duplication" and ~ "without needing to resort to separate ...
Jason Gross's user avatar
  • 1,537
3 votes
1 answer

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

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
  • 3,070