Email Gateway (Aug 18 2022 at 09:32): Email Gateway (Aug 18 2022 at 09:32):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Marco,
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
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 09:32):From: Makarius <makarius@sketis.net>
Actually this is the current internal development version. The official
Isabelle2005 source reads like this:
(* renames and reverses the strings in vars away from names *)
fun rename_aTs names vars : (string*typ)list =
let fun rename_aT (vars,(a,T)) =
(variant (map #1 vars @ names) a, T) :: vars
in Library.foldl rename_aT ([],vars) end;
fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
In general there are usually two steps to find out what a certain internal
operation does:
1) look at the definition
2) look at the actual uses elsewhere
(Use something like grep -r --include=\*.ML here.)
Makarius
Email Gateway (Aug 18 2022 at 09:36):From: Marco <marco@uma.pt>
Could someone please tell me what rename_wrt_term does?
Last updated: May 03 2024 at 08:18 UTC