Closed randomguy3 closed 11 years ago
We want to be able to have data that is just "there", but never seen (eg: Isabelle context). This should never be serialised, and is not necessarily unifiable (what should happen on rewrites?)
This should be doable currently. Theories have complete control over what data is serialised and how unification happens.
We want to be able to have data that is just "there", but never seen (eg: Isabelle context). This should never be serialised, and is not necessarily unifiable (what should happen on rewrites?)