Searched refs:mk_var (Results 201 - 225 of 368) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DSmtLib.sml75 (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 DmungeTools.sml279 (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 DnumSimps.sml53 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 DbinderLib.sml223 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 Dsexp.sml245 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 Dsexp.sml245 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 DgrammarLib.sml328 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 Dcheri_stepLib.sml21 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 DdimacsTools.sml176 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 DEmitML.sml85 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 DhhTranslate.sml82 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 Dmonadsyntax.sml342 val m1 = mk_var("m1", m1ty)
343 val m2 = mk_var("m2", m2ty)
/seL4-l4v-10.1.1/HOL4/src/string/
H A DstringScript.sml28 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 DupdateLib.sml387 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 Dlisp_evalScript.sml28 INST [``limit:num``|->``l:num``,mk_var("eip",``:word32``) |-> mk_var("p",``:word32``)]
/seL4-l4v-10.1.1/HOL4/examples/CCS/
H A DCCSConv.sml152 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 DdecompTools.sml159 val g = inst [alpha|->p_ty] (mk_var("g",mu_ty))
160 val avar = mk_var("a",stringLib.string_ty)
H A DnormalFormsTest.sml32 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 DConv.sml689 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 DregAllocation.sml870 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 DregAllocation.sml870 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 DregAllocation.sml870 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 Dcompiler.sml223 val cvar = mk_var(new_name, ctype)
/seL4-l4v-10.1.1/HOL4/examples/
H A Ddpll.sml184 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 Darm_progScript.sml136 else Term.mk_var (s ^ Int.toString i, Type.bool))

Completed in 584 milliseconds

1234567891011>>