Dear all, I would like Isabelle/HOL to parse types named by numerals (only natural numbers). The type `4` should represent a type inhabited by exactely 4 elements. Generally The type n, for n a numeral positive integer representation, the type `n` should represent a type with exactly $n$ elements, where $n$ is the number encoded in n.
Is there any chance to have this? Amine.
