/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | SmtLib.sml | 75 (Term.mk_var ("x", intSyntax.int_ty), Lib.apfst (fn tm => 101 (Term.mk_var ("x", realSyntax.real_ty), Lib.apfst (fn tm => 130 (Term.mk_var ("x", wordsSyntax.mk_word_type Type.alpha), Lib.apfst (fn tm =>
|
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | mungeTools.sml | 279 (mk_var(nm2,ty) |-> mk_var(nm1,ty)) :: acc 298 | SOME newname => ALPHA_CONV (mk_var(newname,vty)) t
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | numSimps.sml | 53 val x = mk_var("x", num_ty) 54 val y = mk_var("y", num_ty) 557 val base_rewrite = INST [mk_var ("m", num) |-> v] SUC_PRE
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/basics/ |
H A D | binderLib.sml | 223 val new_t = mk_var(newname, type_of new_in_thm) 392 val apm = mk_var("apm", mk_perm_ty rng_ty) 521 val f_t = mk_var(fstr, type_of f_t0)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | sexp.sml | 245 val qtm' = subst [f |-> mk_var(name,fty)] qtm 898 `^(mk_var 1287 (* mlsym(pkg,nam) |--> mk_var("pkg::nam",``:sexp``) *) 1290 mk_var(mlsym_to_string sym,``:sexp``) 1296 (* mlsym(pkg,nam) ty |--> mk_var("pkg::nam",ty) *) 1299 mk_var(mlsym_to_string sym,ty) 1329 mk_var(sym_string,ty)) 1739 mk_var(hol_name, ty) 1765 else ALPHA_CONV (mk_var(hol_vname, vty)) tm 1872 val newvar = mk_var(sym_nam [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | sexp.sml | 245 val qtm' = subst [f |-> mk_var(name,fty)] qtm 898 `^(mk_var 1287 (* mlsym(pkg,nam) |--> mk_var("pkg::nam",``:sexp``) *) 1290 mk_var(mlsym_to_string sym,``:sexp``) 1296 (* mlsym(pkg,nam) ty |--> mk_var("pkg::nam",ty) *) 1299 mk_var(mlsym_to_string sym,ty) 1329 mk_var(sym_string,ty)) 1739 mk_var(hol_name, ty) 1765 else ALPHA_CONV (mk_var(hol_vname, vty)) tm 1872 val newvar = mk_var(sym_nam [all...] |
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/ |
H A D | grammarLib.sml | 328 val t = variant used (mk_var(appletter aty, aty)) 434 new_definition (defn_name, mk_eq(mk_var(gname, gty), grammar_t)) before
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/cheri/step/ |
H A D | cheri_stepLib.sml | 21 val w = Term.mk_var ("w", wordsSyntax.mk_int_word_type 32) 247 fun x i = Term.mk_var ("x" ^ Int.toString i, Type.bool)
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/ |
H A D | dimacsTools.sml | 176 then mk_var(((!prefix) ^ Int.toString n), Type.bool) 177 else mk_neg(mk_var(((!prefix) ^ Int.toString(Int.abs n)), Type.bool));
|
/seL4-l4v-10.1.1/HOL4/src/emit/ |
H A D | EmitML.sml | 85 val a = mk_var("a",bool) 86 val b = mk_var("b",bool) 102 fun mk_record_vconstr (name,ty) = mk_var(name^"--Record Constr Var",ty) 205 map (fn (i,ty) => mk_var("v"^Int.toString i,ty)) (Lib.enumerate 0 alist); 236 val pvar = mk_var("^" ^ fst(dest_const c), 914 val fns = map (fn upd_t => mk_var ("f", #1(dom_rng (type_of upd_t)))) upds 918 mk_var("v"^int_to_string n,ty) :: acc) 945 mk_var("v"^int_to_string n,ty) :: acc)
|
/seL4-l4v-10.1.1/HOL4/src/holyhammer/ |
H A D | hhTranslate.sml | 82 let val r = mk_var ("f" ^ string_of_genvar iref, ty) in 88 let fun f i ty = mk_var ("X" ^ int_to_string i, ty) in
|
/seL4-l4v-10.1.1/HOL4/src/monad/ |
H A D | monadsyntax.sml | 342 val m1 = mk_var("m1", m1ty) 343 val m2 = mk_var("m2", m2ty)
|
/seL4-l4v-10.1.1/HOL4/src/string/ |
H A D | stringScript.sml | 28 let val n = mk_var("n",num) 61 if n < 256 then n else FAIL ORD ^(mk_var("> 255", bool)) (CHR n)`,
|
/seL4-l4v-10.1.1/HOL4/src/update/ |
H A D | updateLib.sml | 387 val x = Term.mk_var ("x", uty) 388 val y = Term.mk_var ("y", uty)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_evalScript.sml | 28 INST [``limit:num``|->``l:num``,mk_var("eip",``:word32``) |-> mk_var("p",``:word32``)]
|
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | CCSConv.sml | 152 val U = mk_var ("u", type_of (hd actl)); 302 val U = mk_var ("u", type_of (hd actl));
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | decompTools.sml | 159 val g = inst [alpha|->p_ty] (mk_var("g",mu_ty)) 160 val avar = mk_var("a",stringLib.string_ty)
|
H A D | normalFormsTest.sml | 32 fun ith_var ty i = mk_var ("v" ^ int_to_string i, ty); 34 val P = mk_var ("P", num --> num --> bool);
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Conv.sml | 689 val P = mk_var {Name = Pname, Ty = ty} 690 val Q = mk_var {Name = Qname, Ty = ty} 1526 val fv = mk_var {Name = Name, Ty = List.foldr mkfty Ty xs} 1587 val x = variant vars (mk_var {Name = varnm, Ty = ty1}) 1651 val f = mk_var {Name = "f", Ty = alpha --> bool} 2203 val b = Term.mk_var ("b", Type.bool) 2337 val P = mk_var {Name = "P", Ty = alpha-->bool} 2370 val x = mk_var {Name = "x", Ty = ty} 2371 and y = mk_var {Name = "y", Ty = ty} 2372 and z = mk_var {Nam [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | regAllocation.sml | 870 List.map (fn n => {redex = mk_var (T.look(!tmpTable,n), tp), 871 residue = mk_var ("r" ^ Int.toString (T.look(!color,n)), tp)}) 875 List.map (fn n => {redex = mk_var (T.look(!tmpTable,n), tp), 876 residue = mk_var ("m" ^ Int.toString(T.look(!memT,n)), tp)})
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | regAllocation.sml | 870 List.map (fn n => {redex = mk_var (T.look(!tmpTable,n), tp), 871 residue = mk_var ("r" ^ Int.toString (T.look(!color,n)), tp)}) 875 List.map (fn n => {redex = mk_var (T.look(!tmpTable,n), tp), 876 residue = mk_var ("m" ^ Int.toString(T.look(!memT,n)), tp)})
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | regAllocation.sml | 870 List.map (fn n => {redex = mk_var (T.look(!tmpTable,n), tp), 871 residue = mk_var ("r" ^ Int.toString (T.look(!color,n)), tp)}) 875 List.map (fn n => {redex = mk_var (T.look(!tmpTable,n), tp), 876 residue = mk_var ("m" ^ Int.toString(T.look(!memT,n)), tp)})
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | compiler.sml | 223 val cvar = mk_var(new_name, ctype)
|
/seL4-l4v-10.1.1/HOL4/examples/ |
H A D | dpll.sml | 184 fun mk_index s i = mk_var(s ^ "_" ^ Int.toString i, bool)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/prog/ |
H A D | arm_progScript.sml | 136 else Term.mk_var (s ^ Int.toString i, Type.bool))
|