Re: [isabelle] Hiding import of SList
-----BEGIN PGP SIGNED MESSAGE-----
I use the no_notation command for this kind of thing, for example to
overwrite the "+" symbol:
no_notation plus (infixl "+" 65)
consts "myplus" :: "nat => nat => nat"
notation "myplus" (infixl "+" 65)
defs myplus: "a + b == ..."
I imagine you can do the same kind of thing to get the original List
notation as you want it.
Denis Bueno wrote:
> Hi all,
> 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
> be qualified.
> 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
> then 
> 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?
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.7 (GNU/Linux)
Comment: Using GnuPG with Fedora - http://enigmail.mozdev.org
-----END PGP SIGNATURE-----
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