Questions tagged [definition]
The definition tag has no usage guidance.
1
question
4
votes
2
answers
148
views
Coq defining a hierarchy of collections of integers with infinitely many "levels"
I'm trying to formalize a small part of higher-order arithmetic in Coq as an exercise (Wikipedia article for second-order arithmetic).
It's straightforward to formalize something resembling second-...