referential-equivalence-first-draft #4
Loading…
Reference in New Issue
No description provided.
Delete Branch "nicolas.meric/Isabelle_DOF:referential-equivalence-first-draft"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
Implement built-ins referential equivalence
for the built-ins term annotations (TA)
class instances without checking the instances type.
It must be avoided for certification
A major refactoring of code should be done to enable
referential equivalence for termrepr, by changing the dependency
between the Isa_DOF theory and the Assert theory.
The assert_cmd function in Assert should use the value* command
functions, which make the elaboration of the term
referenced by the TA before passing it to the evaluator
and expose some of current implementation limitations