Searched refs:mk_var (Results 76 - 100 of 368) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/HolQbf/
H A DQDimacs.sml199 fun mk_var s = function
233 boolSyntax.mk_neg (mk_var (String.extract (s, 1, NONE)))
235 mk_var s
242 (boolSyntax.list_mk_forall o Lib.## (map mk_var, prefix) o split0) xs
244 (boolSyntax.list_mk_exists o Lib.## (map mk_var, prefix) o split0) xs
H A Dselftest.sml83 fun f n = Term.mk_var("v"^(Int.toString n),Type.bool)
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DboolSimps.sml337 val x = mk_var("x", alpha)
338 val x' = mk_var("x'", alpha)
339 val y = mk_var("y", beta)
340 val y' = mk_var("y'", beta)
341 val f = mk_var("f", alpha --> beta --> gamma)
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A DImport.sml238 Term.mk_var (f, typ) (* for recursion *)
251 Term.mk_var (c, typ) (* for recursion *)
262 fun AVar ty = Term.mk_var ("_" ^ anonSuffix(), Ty ty)
265 fun Var (v, ty) = Term.mk_var (v, Ty ty)
267 fun uVar v = Term.mk_var (v, oneSyntax.one_ty)
268 fun bVar v = Term.mk_var (v, Type.bool)
269 fun nVar v = Term.mk_var (v, numSyntax.num)
270 fun iVar v = Term.mk_var (v, intSyntax.int_ty)
271 fun sVar v = Term.mk_var (v, stringSyntax.string_ty)
272 fun vVar v = Term.mk_var (
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A Dderive_specsLib.sml36 |> filter (fn tm => cdr (car tm) = mk_var("p",``:word32``))
97 |> filter (fn tm => cdr (car tm) = mk_var("p",``:word32``))
331 val i = [mk_var("eip",``:word32``) |-> mk_var("p",``:word32``),
332 mk_var("rip",``:word64``) |-> mk_var("p",``:word64``)]
340 val new_p = subst [mk_var("n",``:num``)|-> numSyntax.mk_numeral (Arbnum.fromInt y)] pattern
341 val th = INST [mk_var("p",type_of new_p)|->new_p] th
362 val pc_var1 = mk_var("pc",``:word32``)
363 val pc_var2 = mk_var("
[all...]
H A DstraightlineLib.sml46 |> map (fn v => v |-> mk_var(fst (dest_var v) ^ postfix,type_of v))
79 in if length t > 1 then mk_var (hd t,ty) else fail() end
/seL4-l4v-10.1.1/HOL4/src/1/
H A DPrim_rec.sml418 mk_var(pass Name, Ty)
431 val v = num_variant away (mk_var(vname, fty))
435 val v = mk_var(case_constant_name{type_name = Tyop},
706 local val P = mk_var("P", alpha --> bool)
1066 local val A = mk_var("A",Type.bool)
1067 val B = mk_var("B",Type.bool)
1169 (mk_var(s^(Int.toString n),h))
1175 [variant avoid (mk_var(s, hd tys))]
1233 RAND_CONV (ALPHA_CONV (mk_var(vnm^vnm, ty))) t
1282 val M = variant allvars (mk_var("
[all...]
H A DDiskFilesHeader.sml42 ptm_v (s, tyn) => mk_var(s, types ! tyn)
H A DRsyntax.sig8 val mk_var : {Name:string, Ty:hol_type} -> term value
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/
H A DMutRecDef.sml309 (mk_var {Name = "x"^(int_to_string var_num),
324 let val recvar = mk_var {Name = "rec"^(int_to_string type_case_num),
335 (mk_var {Name = "x"^(int_to_string var_num),
404 val Joint_x = mk_var {Name = "x", Ty = joint_type}
413 arg = mk_select{Bvar = mk_var{Name = "x", Ty = ty},
535 val constructor = mk_var {Name = name, Ty = constructor_type}
539 let val v = mk_var{Name = ("x"^(int_to_string n)), Ty = ty}
763 val JointProp = mk_var{Name = "Prop",
766 fun new_ty_Prop type_name = mk_var{Name = type_name^"_Prop",
843 val case_var = mk_var{Nam
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A DmechReasoning.sml110 mk_var ("v" ^ (i := !i + 1; Int.toString (!i)) , Type `:DATA`)
192 fun new_var() = (i := !i + 1; mk_var ("v"^Int.toString (!i), Type`:DATA`))
344 let val st = mk_pair (mk_var ("regs", Type `:REGISTER |-> DATA`),
345 mk_var ("mem", Type `:ADDR |-> DATA`))
393 val st' = mk_var ("st", Type `:DSTATE`);
464 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`);
569 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`);
570 val st = mk_var ("st", Type `:DSTATE`);
648 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`);
810 val st = mk_var ("s
[all...]
/seL4-l4v-10.1.1/HOL4/src/n-bit/
H A DbitstringLib.sml347 Term.mk_var ("n" ^ (if j + 1 = i then "" else Int.toString (i-1-j)),
411 val w = Term.mk_var ("w", ty)
414 val f = Term.mk_var (boolify_lhs, Type.--> (ty, Term.type_of boolify_rhs))
417 fun mk_b j = Term.mk_var ("b" ^ Int.toString (i-1-j), Type.bool)
422 val f = Term.mk_var (bitify_lhs,
441 val x = Term.mk_var ("x", Term.type_of btuple)
/seL4-l4v-10.1.1/HOL4/src/new-datatype/
H A DNDatatype.sml73 all_thm = REFL (mk_comb(all, mk_var("x", tyvar))),
265 val x = mk_var("x", alpha);
266 val Jsome_tm = mk_abs(x, mk_abs(mk_var("u", one_ty),
309 val KT = mk_abs(mk_var("x", alpha), T);
317 |-> mk_var("ok_"^s, self-->bool)]
371 val oks = map (fn s=>mk_var("ok_"^s, rng-->bool)) ty_names
/seL4-l4v-10.1.1/HOL4/examples/lambda/barendregt/
H A DlabelledTermsScript.sml35 val LAM_t = mk_var("LAM", ``:string -> ^newty -> ^newty``)
44 val LAMi_t = mk_var("LAMi", ``:num -> string -> ^newty -> ^newty -> ^newty``)
54 val APP_t = mk_var("APP", ``:^newty -> ^newty -> ^newty``)
70 val VAR_t = mk_var("VAR", ``:string -> ^newty``)
116 val t = mk_var("t", newty)
158 val t = mk_var("t", ty)
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DcommonTools.sml38 let val x = mk_var("x",type_of rhs )
138 val mk_var = Term.mk_var; value
144 fun mk_bool_var v = mk_var(v,bool);
172 fun prime v = mk_var((term_to_string2 v)^"'",type_of v)
176 fun unprime v = if is_prime v then mk_var(implode(butlast(explode(term_to_string2 v))),type_of v) else v
H A DstringBinTree.sml121 mk_var("x",``:char list``))),
151 val tree = mk_let(mk_abs(mk_var("x",``:char list``),
154 in mk_abs(mk_var("t",``:string``),if isSome abs then mk_pabs(valOf abs,tree) else tree) end
172 val k3 = List.map (fn s => (s,mk_var(s,``:bool``))) ap;
/seL4-l4v-10.1.1/HOL4/src/HolSat/
H A DminisatResolve.sml24 val A = mk_var("A",bool)
25 val B = mk_var("B",bool)
/seL4-l4v-10.1.1/HOL4/src/bag/
H A DbagSimps.sml82 val x = mk_var("x", bag_ty)
83 val y = mk_var("y", bag_ty)
/seL4-l4v-10.1.1/HOL4/src/real/
H A DrealSimps.sml140 val nvs = map (fn (t,_) => mk_var(#1 (dest_var t), numSyntax.num)) vs
155 val x = mk_var("x", real_ty)
156 val y = mk_var("y", real_ty)
157 val z = mk_var("z", real_ty)
158 val u = mk_var("u", real_ty)
159 val v = mk_var("v", real_ty)
222 val n = mk_var("n", numSyntax.num)
223 val m = mk_var("m", numSyntax.num)
/seL4-l4v-10.1.1/HOL4/src/string/
H A DstringLib.sml141 val f = Term.mk_var (name, stringSyntax.string_ty --> ty)
154 val f = Term.mk_var (name, ty --> stringSyntax.string_ty)
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/
H A Darm_evalScript.sml146 fun reg n = mk_var ("r" ^ Int.toString n, ``:word32``)
175 fun psr n = mk_var ("r" ^ Int.toString n, ``:ARMpsr``)
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Dselftest.sml66 fun flag tm = mk_var (fst (dest_const tm), bool);
67 fun spsr_flag tm = mk_var ("s" ^ fst (dest_const tm), bool);
95 val GE = mk_var ("GE", ``:word4``);
96 val spsrGE = mk_var ("spsrGE", ``:word4``);
98 val mode = mk_var ("mode", ``:word5``);
99 val spsrmode = mk_var ("spsrmode", ``:word5``);
101 fun reg i = mk_var ("r" ^ Int.toString i, ``:word32``);
120 val mem = mk_var ("mem", ``:word32 -> word8``);
/seL4-l4v-10.1.1/HOL4/examples/elliptic/swsep/
H A DswsepLib.sml74 val new_var1 = prim_variant (free_vars body) (mk_var ("r", ``:word4 -> word32``))
75 val new_var2 = prim_variant (new_var1::free_vars body) (mk_var ("r", ``:word4 -> word32``))
196 val x = mk_var ("x", Type `:word4`);
234 val fe_var = mk_var ("fe", Type `:word4 -> word32`);
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/decompiler/
H A Darm8_decompLib.sml10 fun w_var i = Term.mk_var ("w" ^ Int.toString i, ``:word32``)
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DArith_cons.sml123 fun mk_num_var s = mk_var(s,num_ty);

Completed in 137 milliseconds

1234567891011>>