/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | PairRules.sml | 97 val gfinst = mk_var(fst(dest_var gf),fty) 103 val gxinst = mk_var(fst(dest_var gx),xty) 104 and gyinst = mk_var(fst(dest_var gy),yty) 113 val gpinst = mk_var(fst (dest_var gp),pty) 144 val gfinst = mk_var(fst(dest_var gf), fty) 147 val gxinst = mk_var(fst(dest_var gx), xty) 148 and gyinst = mk_var(fst(dest_var gy), yty) 1500 val f = mk_var("f", alpha --> bool) 1501 val x = mk_var("x", alpha) 1520 val gxinst = mk_var((fs [all...] |
H A D | pairTools.sml | 21 val mk_var = variant fvs o mk_var value 29 val v = mk_var((name_of v)^s,ty) 33 (fn()=> rename_tac v (mk_var(sv^(Int.toString(n())),ty)))
|
/seL4-l4v-10.1.1/HOL4/src/monad/more_monads/ |
H A D | selftest.sml | 91 hd args = mk_var("opt", ``:num option``) andalso
|
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
H A D | patternMatchesSyntax.sml | 33 fn ty => mk_var (next_name (), ty) 265 variant (free_varsl tl) (mk_var("_uv", oneSyntax.one_ty)) 308 val mk_var = mk_var_gen "v" avoid value 318 mk_wc (type_of v) else mk_var (type_of v) 357 AP_THM combinTheory.K_DEF (mk_var("x", alpha)) 620 val x = mk_var ("x", type_of p) 757 fun mk_fake wc = mk_var (GrammarSpecials.mk_fakeconst_name {fake = "_", original = NONE}, type_of wc) 763 variant (free_varsl [pat, guard, rh]) (mk_var("_", oneSyntax.one_ty)) 859 val args = Lib.mapi (fn i => fn ty => mk_var("x" ^ Int.toString i, ty)) argtys
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | wfrecUtils.sml | 111 fn ty => mk_var(pass "v", ty)
|
H A D | Defn.sml | 86 let val P = mk_var("P",bool) 87 val Q = mk_var("Q",bool) 88 val R = mk_var("R",bool) 313 let val M = mk_var("M",bool) 314 val P = mk_var("P",bool) 315 val M1 = mk_var("M1",bool) 685 val fvar = mk_var(fst(dest_var f), 717 val aux_fvar = mk_var(aux_name,itlist(curry(op-->)) (map type_of (R1::SV)) Ty) 748 val fvar = mk_var(fst(dest_var f), 864 val nvs = map (curry mk_var " [all...] |
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/ |
H A D | translationsLib.sml | 839 ((mk_var ("f", ltl_type --> num)) |-> f_term)] new_f_term; 860 val pos_start_term = subst [mk_var("l", type_of var_list_term) |-> var_list_term] pos_start_term; 872 val pos_start_term_concr = subst [mk_var("l", type_of var_list_term) |-> var_list_term] pos_start_term_concr 875 val pos_start_thm_concr = GEN (mk_var ("x", ltl_type)) pos_start_thm_concr; 914 (subst [(mk_var("f", ltl_type --> num) |-> f_term), 915 (mk_var("y", num) |-> term_of_int used_vars_num), 916 (mk_var("n", num) |-> term_of_int n), 917 (mk_var("e", ltl_type) |-> t), 918 (mk_var("m", num --> num) |-> et)] renaming_cond)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | testACL2encoding.ml | 170 (REFL o curry mk_var "a") ``:'a list``); 175 (REFL o curry mk_var "a") ``:'a + num``); 180 (REFL o curry mk_var "a") ``:(num + 'a) list``); 185 (REFL o curry mk_var "a") ``:('a + num) list``);
|
H A D | translateLib.sml | 78 then mk_var(prime((fst o dest_var o var) thm), 81 (mk_var("x",(type_of o sexp_to_term) thm))
|
/seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
H A D | quotient.sml | 195 map Psyntax.mk_var (zip nms tylist) 289 val r = Term.variant (free_vars REL) (mk_var{Name="r", Ty=ty}) 293 val c = Term.variant (free_vars rcl) (mk_var{Name="c", Ty=cty}) 296 val x = Term.variant (free_vars P) (mk_var{Name="x", Ty=ty}) 418 val ty_REP = mk_var{Name = rep, 431 val ty_ABS = mk_var{Name = abs, 442 val r'tm = mk_var{Name="r'", Ty=ty} 447 val atm = mk_var{Name="a", Ty=nty} 482 val x = mk_var{Name="x", Ty=cty} 483 val y = mk_var{Nam [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | funcCall.sml | 110 (mk_plet (mk_var("m" ^ Int.toString(slot) , !VarType), mk_atom r, e), slot + 1)) 117 (mk_plet (r, mk_atom (mk_var("m" ^ Int.toString(slot), !VarType)), e), slot + 1))
|
H A D | refine.sml | 97 (mk_var("v"^Int.toString i,type_of b),p)) plist' 100 val vb4 = mk_var("v"^Int.toString(length plist''), type_of b4)
|
/seL4-l4v-10.1.1/HOL4/src/floating-point/ |
H A D | binary_ieeeSyntax.sml | 77 fun mk_float_var tw = fn v => Term.mk_var (v, mk_float_ty tw) 78 fun mk_ifloat_var tw = fn v => Term.mk_var (v, mk_ifloat_ty tw)
|
/seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
H A D | Witness.sml | 100 (mk_var ("x", (fst o dom_rng o type_of) tm)) 171 (mk_var ("x", type_of b))
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | ThyDataSexp.sml | 136 | Type ty => Term.mk_var("x", ty) :: acc 204 | Type ty => "Y" ^ StringData.encode (tmw (Term.mk_var("x", ty)))
|
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibParameters.sml | 62 val vars = map (fn (n, ty) => (mk_var (vn^"_"^(Int.toString n), ty))) ntL 342 fun mk_new_var (s, ty) = mk_var (s, ty);
|
H A D | selftest.sml | 69 val x = mk_var ("x", numLib.num); 82 val x = mk_var ("x", numLib.num);
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | congLib.sml | 62 val var = mk_var ("x", hol_type) 75 val var = mk_var ("x", hol_type)
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | pseudo_compile.py | 16 (mk_var, mk_plus, mk_uminus, mk_minus, mk_times, mk_modulus, mk_bwand, mk_eq, 40 return mk_var (v_nm, typ) 92 return mk_var (v_nm, typ) 94 vs = [(mk_word32 (j), mk_var (v_nm, typ))
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | codegen_x86Lib.sml | 17 fun foo (i,s) = mk_var("r" ^ int_to_string i,``:word32``) |-> mk_var(s, ``:word32``)
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
H A D | arm_emitScript.sml | 54 FAIL num2register ^(mk_var("30 < n",bool)) n`, 75 FAIL num2condition ^(mk_var("15 < n",bool)) n`,
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/KatiPuzzle/ |
H A D | KatiPuzzleScript.sml | 76 (fn s => mk_var(s,bool)) 167 (mk_var("s",type_of s))
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | SmtLib_Parser.sml | 200 (fn (s, t) => (s, Term.mk_var (s, Term.type_of t), t)) bindings 242 val vars = List.map (fn vT => (Lib.fst vT, Term.mk_var vT)) vars 393 val tm = Term.mk_var (name, 412 val vars = List.map (fn vT => (Lib.fst vT, Term.mk_var vT)) vars 425 val tm = Term.mk_var (name,
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | OmegaSymbolic.sml | 49 val pvar = mk_var("p", bool) 50 val qvar = mk_var("q", bool) 51 val xvar = mk_var("x", int_ty) 170 val p = mk_var("p", c_ty) 207 (REWRITE_RULE [nilth] (INST [mk_var(varname, clist_ty) |-> nil_t] consth),
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/basics/ |
H A D | termScript.sml | 29 val LAM_t = mk_var("LAM", ``:string -> ^newty -> ^newty``) 39 val APP_t = mk_var("APP", ``:^newty -> ^newty -> ^newty``) 53 val VAR_t = mk_var("VAR", ``:string -> ^newty``) 89 val t = mk_var("t", newty) 134 val t = mk_var("t", ty)
|