Questions tagged [definition]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
4 votes
2 answers

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