Searched refs:rename_vars (Results 1 - 17 of 17) sorted by path
| /seL4-l4v-master/HOL4/examples/HolCheck/ |
| H A D | lzConv.sml | 1789 else raise ERR "rename_vars" "Term not a binder"
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
| H A D | stateLib.sig | 36 val rename_vars: value
|
| H A D | stateLib.sml | 902 rename_vars:
907 fun rename_vars (rmap, bump) = function
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/x64/prog/ |
| H A D | x64_progLib.sml | 191 val x64_rename = stateLib.rename_vars (x64_rmap, [])
|
| /seL4-l4v-master/HOL4/examples/lambda/basics/ |
| H A D | nomdatatype.sig | 42 val rename_vars : (string * string) list -> conv value
|
| H A D | nomdatatype.sml | 224 fun rename_vars alist t = let function
|
| H A D | termScript.sml | 426 |> CONV_RULE (DEPTH_CONV (rename_vars [("p_1", "u"), ("p_2", "N")]))
669 |> CONV_RULE (DEPTH_CONV (rename_vars [("p", "fm")]))
|
| /seL4-l4v-master/HOL4/src/1/ |
| H A D | Conv.sml | 2432 else raise ERR "rename_vars" "Term not a binder"
|
| /seL4-l4v-master/HOL4/src/quotient/examples/ |
| H A D | ind_rel.sml | 1272 fun rename_vars (vars::more_vars) vars_to_avoid renamed_vars = function
1282 rename_vars more_vars (new_vars@vars_to_avoid) (new_vars::renamed_vars)
1284 | rename_vars [] _ renamed_vars = rev renamed_vars
1285 val renamed_argvars = rename_vars argvars exists_vars []
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/arm/prog/ |
| H A D | arm_progLib.sml | 422 val arm_rename = stateLib.rename_vars (arm_rmap, ["b"])
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/prog/ |
| H A D | arm8_progLib.sml | 289 val arm_rename = stateLib.rename_vars (arm_rmap, ["b"])
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/m0/prog/ |
| H A D | m0_progLib.sml | 313 val m0_rename = stateLib.rename_vars (m0_rmap, ["b"])
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/mips/prog/ |
| H A D | mips_progLib.sml | 247 val mips_rename = stateLib.rename_vars (mips_rmap, ["b"])
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/prog/ |
| H A D | riscv_progLib.sml | 256 val riscv_rename = stateLib.rename_vars (riscv_rmap, ["b"])
|
| /seL4-l4v-master/HOL4/examples/lambda/barendregt/ |
| H A D | finite_developmentsScript.sml | 603 |> CONV_RULE (DEPTH_CONV (nomdatatype.rename_vars [("p", "n")]) THENC
643 (nomdatatype.rename_vars [("p_1", "n"), ("p_2", "M")]))
741 (rename_vars [("p_1", "n"), ("p_2", "ps")]))
|
| H A D | labelledTermsScript.sml | 414 (rename_vars [("p_1", "u"), ("p_2", "N")]))
|
| /seL4-l4v-master/graph-refine/ |
| H A D | pseudo_compile.py | 440 def rename_vars (function): function
469 rename_vars (fun)
|
Completed in 168 milliseconds