Email Gateway (Aug 22 2022 at 17:15): Email Gateway (Aug 22 2022 at 17:15):From: Joshua Chen <joshua.chen@uni-bonn.de>
Dear all,
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.
Best wishes,
Josh
Email Gateway (Aug 22 2022 at 17:16):From: Makarius <makarius@sketis.net>
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
Last updated: May 07 2024 at 01:07 UTC