Re: [isabelle] rename_wrt_term

On Mon, 7 Aug 2006, Florian Haftmann wrote:

> > Could someone please tell me what rename_wrt_term does? 
> > fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)

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.)


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