Email Gateway (Aug 18 2022 at 10:23): Email Gateway (Aug 18 2022 at 10:23):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Randy Pollack wrote:
Even though I have "show sorts" on, [] is not shown with a type, but
I've also noticed this - presumably the thinking is, that if a user has
declared a constant, he/she knows what type it is.
But often I've found it would be helpful, when a polymorphic constant is
used monomorphically (or with a less general polymorphic type) in a
theorem, it would be nice to be able to see the type.
Apart from printing out the term (which can give rather long output) is
there any way of doing this?
Jeremy
Email Gateway (Aug 18 2022 at 10:23):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
This is indeed a problem, including the need to type cast constants
frequently in local goals to ensuring
matching to global goals.
A useful flag is the show constants flag, this at least gives you a
list of the constants in the goal state and
their types, but not of which instance is which in the actual goals.
Specialised syntax for type casting constants is useful. eg
syntax
"_empty" :: "type \<fun> logic" ("{}[_]")
translations
"{}[T]" => "{}::T set"
This sort of syntax helps clarify the instantiated type parameters
and saves clutter.
A suitable typed print translation will allow this operator to appear
in the goal state display too.
This is, of course, a lot of effort!
Some automatic support for declaring such instantiation syntax for
every generic constant would be useful.
Brendan
Dr Brendan Mahony
C3I Division ph +61 8 8259 6046
Defence Science and Technology Organisation fx +61 8 8259 5589
Edinburgh, South Australia Brendan.Mahony@dsto.defence.gov.au
Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.
IMPORTANT: This email remains the property of the Australian Defence Organisation 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.
Last updated: May 03 2024 at 04:19 UTC