[isabelle] The purpose of types is to be a front end for sets

This is to exercise the list server hard drive, and make sure it doesn't freeze up, it being wet and damp in England, where the Isabelle list server doesn't get used much, as opposed to sunny in France, where the Coq list server gets used more.

As long as the outlook is sunny, the sum ((2000 + 2999)::nat) is both an element of 5000 and a subset of 5000, as shown by the attached screenshot. And (5000::nat) is both equal to 5000 and a subset of 5000.

Try this at home:

theorem "1 \<in> 5000"

Thanks to Andreas for these:

declare [[coercion_enabled]]
declare [[coercion NH⇣C]]


Attachment: 130507_nat_to_sT_coercion.png
Description: PNG image

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.