Re: [isabelle] Sublocale, subclass and execution.



Hi Florian,

Thanks for the feedback.  Here are two quick questions:

> 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.

> One key property is that »t« is parsed in the (approximate) syntactic
> context of expr (like mixin equations also).  Let »t'« denote the
> internalized term.  Then we have:
>
> definition
>   f_def: "f = t'"
>
> permanent_interpretation prefix: expr
>   -- ‹with implicit mixin: f_def [symmetric]›

This, I guess, refers to the original sublocale command, right?

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.

Clemens





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