Searched refs:ren (Results 1 - 7 of 7) sorted by path
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/c_output/ |
| H A D | c_outputLib.sml | 466 val ren = enumerate 1 args_list; value
467 val ren' = map (fn (n, t) =>
468 ({redex=t, residue = mk_var ("a"^(Int.toString n), word_type)})) ren;
470 Thm.INST ren' def'
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Pmatch.sml | 710 fun rename_top_bound_vars ren cs = (
714 | COMB (t1, t2) => mk_comb (rename_top_bound_vars ren t1, rename_top_bound_vars ren t2)
716 let val cs' = rename_bvar (Lib.assoc v ren) cs handle HOL_ERR _ => cs
718 val t'' = rename_top_bound_vars ren t'
773 val ren = pat_match3 fvs pat_exps pats (* better pats than givens patts3 *) value
774 in (rename_top_bound_vars ren case_tm)
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | normalForms.sml | 146 fun ren _ [tm] [] = tm function
147 | ren avoid (b :: a :: dealt) (INL NONE :: rest) =
148 ren avoid (mk_comb (a, b) :: dealt) rest
149 | ren avoid (b :: dealt) (INL (SOME v) :: rest) =
150 ren avoid (mk_abs (v, b) :: dealt) rest
151 | ren avoid dealt (INR (sub, tm) :: rest) =
153 CONST _ => ren avoid (tm :: dealt) rest
154 | VAR _ => ren avoid (subst sub tm :: dealt) rest
156 ren avoid dealt (INR (sub, a) :: INR (sub, b) :: INL NONE :: rest)
165 ren (inser
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
| H A D | patternMatchesLib.sml | 3311 fun rename_uscore_vars ren avoid [] = ren
3312 | rename_uscore_vars ren avoid (v::vs) =
3318 rename_uscore_vars ((v |-> v')::ren) (v'::avoid) vs
3319 end handle HOL_ERR _ => rename_uscore_vars ren avoid vs
3394 val ren = rename_uscore_vars [] avoid to_ren value
3396 subst ren vars_tm0
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | syntax.py | 765 def ren (expr): function in function:rename_expr_substor
770 return ren
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Normalize.sml | 723 fun ren (v,(a,s)) = function
732 val (_,sub) = NameSet.foldl ren (avoid,Subst.empty) captured
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Normalize.sml | 723 fun ren (v,(a,s)) = function
732 val (_,sub) = NameSet.foldl ren (avoid,Subst.empty) captured
|
Completed in 157 milliseconds