Re: [isabelle] Hiding import of SList



-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

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.

best,
lucas

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"
> primrec
>   "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

iD8DBQFIKGPuiUn2r+81A2gRAlFTAJwOFey3pjJpY9nD0roGRvVUw4cO9wCeI+jV
/erb5NhNCEzvYlNuLBOD+7E=
=lxYN
-----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 MHonArc.