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,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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