Re: [isabelle] Function Definitions Within Locales

Hi Matej,

> I hope you don't mind a question about locales:
> Is it possible to provide function definitions within locales (before
> the 'assumes' block)?
> Some of my locale's assumptions refer to functions which need not be
> locale parameters. I want to provide full definitions for such functions
> within the locale (after the parameters and before the assumptions).

This in the strictest sense is not possible.  You can circumvent this in
one of the following ways.

a) Introduce intermediate locale where you just define the function
formally and then import this locale into the main locale with
assumptions about the function

b) Turn the function itself into a parameter of the locale and assume
its desired properties explicitly.

It depends on what you want to model which option makes more sense.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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