Email Gateway (Aug 18 2022 at 17:47): Email Gateway (Aug 18 2022 at 17:47):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
Apologies for what may be a trivial question, but a quick look through the HOL sources and this list has not offered anything useful examples.
I have a a locale topology (many details omitted) with an interpretation real_top: topology "UNIV::real set" "real_top"
I also have a locale continuous_fun = A: topology A S + B: topology B S fixes f :: "'a => 'b".
When I try to
interpret continuous_fun A S "UNIV::real set" "real_top" f
I get an unhelpful error message
exception DUP ...
which seems to be complaining that the real_top interpretation is being duplicated. If I instead use
interpret continuous_fun A S "UNIV::real set" "id real_top"
there is no problem with DUP, but of course I don't have exactly the interpretation I want.
Is there any way to get around this DUP exception?
Brendan
Dr Brendan Mahony
C3I Division ph +61 8 7389 6046
Defence Science and Technology Organisation fx +61 8 7389 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 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 17:47):From: Clemens Ballarin <ballarin@in.tum.de>
Quoting "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>:
I have a a locale topology (many details omitted) with an
interpretation real_top: topology "UNIV::real set" "real_top"I also have a locale continuous_fun = A: topology A S + B: topology
B S fixes f :: "'a => 'b".
This is not well-formed. You probably want something like
locale cont = A: top A S + B: top B S for A B S + fixes f ...
You may use print_locale cont to check if the locale has the desired
parameters.
When I try to
interpret continuous_fun A S "UNIV::real set" "real_top" f
I get an unhelpful error message
exception DUP ...
which seems to be complaining that the real_top interpretation is
being duplicated.
Please provide an stack trace by setting Topdevel.debug, in Isar
ML_val {* Toplevel.debug := true *}
DUP indicates an error, not duplicate interpretations.
Clemens
Last updated: Apr 23 2024 at 20:15 UTC