[isabelle] baffled by fun error message
When I try the following minimal example in Isabelle2015
datatype (funs : 'f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
type_synonym ('f, 'v) trs = "(('f, 'v) term Ã ('f, 'v) term) set"
fixes F and R :: "('f, 'v) trs"
assumes "R â F"
fun star :: "('f, 'v) term â ('f, 'v) term"
"star (Fun f ts) = Fun f (map star ts)"
I get the error message:
exception THM 0 raised (line 744 of "thm.ML"):
forall_intr: variable "R" free in assumptions
wf R â
(âf ts x. x â set ts â (x, Fun f ts) â R) â
âx. Wellfounded.accp star_rel x
[star_rel â ??.Test.star_rel]
Which leaves me quite puzzled. I do neither understand the error
message nor why there is an error at all. Can somebody explain what
happens here, please?
This archive was generated by a fusion of
Pipermail (Mailman edition) and