Re: [isabelle] Morphism locales and interpretations [SEC=UNCLASSIFIED]



Quoting "Dr. Brendan Patrick Mahony" <brendan.mahony at 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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.