Re: [isabelle] Generic context data methods



On 10/05/18 14:19, Joshua Chen wrote:
> 
> What exactly are the methods get, put and map (for the signatures
> Theory_Data and Proof_Data) supposed to implement? I roughly get the
> idea of empty, extend, merge and init but am not sure about the generic
> context methods.

These functions (not methods) are the standard ones to access record
fields abstractly.

The "implementation" manual section 1.1 has more explanations about
context data, including some examples.


The type Context.generic alone is not very special: it is just a
disjoint sum of theory + Proof.context, but in practice it usually
occurs with local_theory data, and that is a slightly different story
involving morphisms on data.

You did not say anything what you are trying to do; it does not make
sense to tell a long story without a clear target.


	Makarius




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