[isabelle-dev] Numbers in Types

Amine Chaieb chaieb at in.tum.de
Wed Apr 2 10:01:26 CEST 2008

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?


More information about the isabelle-dev mailing list