Re: [isabelle] [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation[SEC=UNCLASSIFIED]
- To: isabelle-users at cl.cam.ac.uk
- Subject: Re: [isabelle] [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation[SEC=UNCLASSIFIED]
- From: "Dr. Brendan Patrick Mahony" <brendan.mahony at dsto.defence.gov.au>
- Date: Fri, 19 Aug 2011 10:38:51 +0930
- In-reply-to: <4E4D8FE6.email@example.com>
- References: <4E43CE59.firstname.lastname@example.org> <4E4D8FE6.email@example.com>
I admit to a certain feeling surreality listening in on this exchange.
A blow-by-blow defence and repudiation of strong typing played out in the minutiae of Isabelle's reasoning mechanisms.
It is especially amusing as I would also find it useful to distinguish predicates from boolean-valued operators :-), using /\ ,\/ instead of cap,cup etc.
Surely Isabelle-HOL is a logic for those who believe in the value of strong typing and are willing to wear the need to use explicit type coercions?
IMPORTANT: This email remains the property of the Department of Defence and is subject to the jurisdiction of section 70 of the Crimes Act 1914. If you have received this email in error, you are requested to contact the sender and delete the email.
This archive was generated by a fusion of
Pipermail (Mailman edition) and