Re: [isabelle] transfer / lifting / quotient - questions
Equality is executable only on types with an instance of the equal type class (similar to
Haskell's Eq type class). The command datatype automatically makes new types instances of
equal. Since same_size_tree has been defined by other means (the quotient package), you
have to do the instantiation manually. Something along the following lines should work
value "Abs (leaf 0) = Abs (leaf 1)"
The command fails with:
Type same_size_tree not of sort equal
No type arity same_size_tree :: equal
Is there something I can do about this?
Will this cause issues, if I want to generate code?
instantiation same_size_tree :: equal begin
lift_definition equal_same_size_tree :: "tree => tree => bool"
is "%t1 t2. size t1 = size t2"
instance by intro_classes(transfer, simp add: tree_equivp_def)
PS: I leave the Nitpick question to nitpick experts.
This archive was generated by a fusion of
Pipermail (Mailman edition) and