forked from Isabelle_DOF/Isabelle_DOF
Support invariants on attributes of classes atttributes. Example: doc_class inv_test1 = a :: int doc_class inv_test2 = b :: "inv_test1" c:: int invariant inv_test2 :: "c σ = 1" invariant inv_test2' :: "a (b σ) = 2" doc_class inv_test3 = inv_test1 + b :: "inv_test1" c:: int invariant inv_test3 :: "a σ = 1" invariant inv_test3' :: "a (b σ) = 2" To support invariant on attributes in attributes and invariant on attributes of the superclasses, we check that the type of the attribute of the subclass is ground:› ML‹ val Type(st, [ty]) = \<^typ>‹inv_test1› val Type(st', [ty']) = \<^typ>‹'a inv_test1_scheme› val t = ty = \<^typ>‹unit› › |
||
---|---|---|
.. | ||
document-templates | ||
DOF | ||
ontologies | ||
scala | ||
tests | ||
ROOT | ||
ROOTS |