Re: [isabelle] Wellsortedness error by using user defined function in quickcheck
Now I've got a new problem to give a code attribute for the following function.
"funimage r x = (THE y. (x, y) ∈ r)"
I give a weaker version of code definition, i.e
(funimage (set ss) x) = snd (hd (filter (λ (x0, y0). x = x0) ss))
but I don't know how to represent it equivalently in list, because it addresses that y is unique and x : r, which returns boolean type.
I wonder if there is undefined value for list to represent the invalid case, e.g. return the invalid value when y is not unique. Also I'm trying to giving assumptions for the the code attribute, which is
"x : Domain (set ss) ==> functional (set ss) ==> (funimage (set ss) x) = snd (hd (filter (λ (x0, y0). x = x0) ss))"
Then I receive a warning "Not a equation".
How can I deal with it ? Thanks for helps.
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
This archive was generated by a fusion of
Pipermail (Mailman edition) and