Re: [isabelle] Hiding import of SList
An aside: It is usually better to avoid tests on lists like "any".
Instead of "any f xs" write "EX x:set xs. f x". Because now the existing
automation for quatifiers and sets will kick in automatically.
Denis Bueno wrote:
I have a theory (attached) which imports Main and LList2 (available
from afp). LList2 imports LList which imports SList, and the
importing of SList makes defining recursive functions over normal
lists (from List) very difficult, because it seems all names have to
The following, for example, is not admitted due to a type clash:
consts zipn :: "'a List.list List.list => 'a List.list List.list"
any :: "('a => bool) => 'a List.list => bool"
"any f List.Nil = False"
"any f (List.Cons x xs) = (if f x then True else any f xs)"
"zipn xss = (if any (%x. x = List.Nil) xss
else List.Cons (map hd xss) (zipn (map tl xss)))"
Can I hide all SList-related stuff so I don't have to play games and
qualify every list-related function I call?
This archive was generated by a fusion of
Pipermail (Mailman edition) and