Re: [isabelle] Sublocale, subclass and execution.

Hi Clemens,

sorry for the delay.

On 16.10.2014 18:57, Clemens Ballarin wrote:

>> permanent_interpretation prefix: expr
>>   where f = t
> What if expr contains where clauses?  Sublocale distinguishes this (awkwardly) by slightly different syntax: "where" <term> "=" <term> within the expression vs. "where" <term> for the rewrite morphism.

This was my fault.  The syntax (cf.
src/Tools/permanent_interpretation.ML) is

permanent_interpretation expr …
  defining …
  where …

>> permanent_interpretation prefix: expr
>>   -- ‹with implicit mixin: f_def [symmetric]›
> This, I guess, refers to the original sublocale command, right?

In a locale context, yes.

> I wonder whether we can come up with a syntax that permits both rewrite morphisms and definitions.  Obviously one of the two kinds of equations would have to be turned around.  Probably it would be more intuitive to reverse the notation of the rewrite morphisms.

Currently, definitions are orientated the other way round than bare
equations.  Not sure what would fit best here.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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