Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] The purpose of types is to be a front end for ...

view this post on Zulip Email Gateway (Aug 19 2022 at 10:59):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
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]]

Regards,
GB
130507_nat_to_sT_coercion.png

Last updated: Apr 20 2024 at 12:26 UTC