Re: [isabelle] prove countability of a new finite type
the theory Countable in HOL/Library, which also defines the countable class, provides the
method countable_datatype to prove instantiations of countable for datatypes automatically.
On 28/05/13 00:24, Roger H. wrote:
datatype Colors = Red | Yellow | Green
How can i prove:
instance Colors :: countable
Mathematically, id say the type is finite, so i would give an injection to the natural numbers. can you help me in isabelle?
This archive was generated by a fusion of
Pipermail (Mailman edition) and