[isabelle-dev] Numbers in Types

[Amine Chaieb]

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