Can we develop a new syntax, say ∑' for sums such that for instance ∑' i : Fin n, i is parsed as ∑ i : Fin n, (i : ℕ) automatically? if we can -- I suspect the answer is positive -- then we don't need to explain the following Hint
Hint "Du: Was bedeutet eigentlich der kleine Pfeil ↑?
Robo: Das ist eine Coersion. Sowas wie wenn man eine natürliche Zahl als ganze Zahl betrachtet,
also die natürliche Abbildung ℕ ↪ ℤ benutzt. Oder hier, wenn ein Element x : Fin n als
Element ↑x : ℕ betrachtet wird."
Ideally we want to override the general notation ∑.
Can we do this for any arithmetic coercion? (not just Fin to ℕ, but say Fin to Int, etc)?
Can we develop a new syntax, say
∑'for sums such that for instance∑' i : Fin n, iis parsed as∑ i : Fin n, (i : ℕ)automatically? if we can -- I suspect the answer is positive -- then we don't need to explain the following HintIdeally we want to override the general notation
∑.Can we do this for any arithmetic coercion? (not just
Fintoℕ, but sayFintoInt, etc)?