Email Gateway (Aug 18 2022 at 18:13): Email Gateway (Aug 18 2022 at 18:13):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
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?
Brendan
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.
Email Gateway (Aug 18 2022 at 18:13):From: Makarius <makarius@sketis.net>
Of course, anybody can join the discussion, either on isabelle-dev or
isabelle-users. See also
http://news.gmane.org/gmane.science.mathematics.logic.isabelle.devel
Please chose exactly one list for your answers, to avoid crossposting and
thus duplication for those on isabelle-dev (which is a subset of
isabelle-users).
Makarius
Last updated: Nov 21 2024 at 12:39 UTC