/seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
H A D | QDimacs.sml | 199 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 D | selftest.sml | 83 fun f n = Term.mk_var("v"^(Int.toString n),Type.bool)
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | boolSimps.sml | 337 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 D | Import.sml | 238 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 D | derive_specsLib.sml | 36 |> 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 D | straightlineLib.sml | 46 |> 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 D | Prim_rec.sml | 418 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 D | DiskFilesHeader.sml | 42 ptm_v (s, tyn) => mk_var(s, types ! tyn)
|
H A D | Rsyntax.sig | 8 val mk_var : {Name:string, Ty:hol_type} -> term value
|
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
H A D | MutRecDef.sml | 309 (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 D | mechReasoning.sml | 110 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 D | bitstringLib.sml | 347 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 D | NDatatype.sml | 73 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 D | labelledTermsScript.sml | 35 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 D | commonTools.sml | 38 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 D | stringBinTree.sml | 121 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 D | minisatResolve.sml | 24 val A = mk_var("A",bool) 25 val B = mk_var("B",bool)
|
/seL4-l4v-10.1.1/HOL4/src/bag/ |
H A D | bagSimps.sml | 82 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 D | realSimps.sml | 140 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 D | stringLib.sml | 141 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 D | arm_evalScript.sml | 146 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 D | selftest.sml | 66 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 D | swsepLib.sml | 74 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 D | arm8_decompLib.sml | 10 fun w_var i = Term.mk_var ("w" ^ Int.toString i, ``:word32``)
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | Arith_cons.sml | 123 fun mk_num_var s = mk_var(s,num_ty);
|