Re: [isabelle] rename_wrt_term



Hi Marco,

> Could someone please tell me what rename_wrt_term does? 

> fun declare_term_names tm =
>   fold_aterms
>     (fn Const (a, _) => Name.declare (NameSpace.base a)
>       | Free (a, _) => Name.declare a
>       | _ => I) tm #>
>   fold_types (fold_atyps (fn TFree (a, _) => Name.declare a | _ => I)) tm;
> 
> fun variant_frees t frees =
>   fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
> 
> fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)

Almost the same as variant_frees ;-). A list of named things ("(string *
'a) list") is renamed so that no name clashes with the names (Frees,
TFrees, base name of constants) in a term.

Hope this helps
Florian
begin:vcard
fn:Florian Haftmann
n:Haftmann;Florian
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at informatik.tu-muenchen.de
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =
	=0D=0A=
	http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i=
	nformatik_tu_muenchen_de.pgp=0D=0A=
	
x-mozilla-html:FALSE
url:http://isabelle.in.tum.de/~haftmann
version:2.1
end:vcard

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.