Thanks Florian for the Word Library Hint. Library/Numeral_Type by Brian is what I need.
I was wondering why it depends on InfiniteSet (ATP_Linkup is perfectly sufficient, I will commit it shortly). Amine. PS: Can't we have metis at earlier stage than ATP_Linkup?. I have experienced many lemmas not proved by blast and auto but within seconds by metis. Amine Chaieb wrote: > 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. > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
