/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | OmegaSimple.sml | 306 else mk_mult(c, mk_var("x"^Int.toString n, int_ty))
|
H A D | OmegaMath.sml | 626 val P_t = mk_var("P", P_ty) 629 val v = mk_var("v"^Int.toString m, bool) 640 else gen_vars (n - 1) (mk_var("v"^Int.toString n, bool)::acc)
|
/seL4-l4v-10.1.1/HOL4/src/marker/ |
H A D | markerLib.sml | 276 fun lb s = mk_var(s, label_ty);
|
/seL4-l4v-10.1.1/HOL4/src/num/ |
H A D | numLib.sml | 186 val mvar = mk_var("m", alpha --> numSyntax.num)
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | parse_type.sml | 19 fun ty_antiq ty = Term.mk_var("ty_antiq",ty)
|
H A D | Parse.sml | 870 val r = mk_var("rcd", d) 883 val f = mk_var("f", hd argtys) handle Empty => raise err 884 val x = mk_var("x", hd (tl argtys)) handle Empty => raise err
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | SharingTables.sml | 252 Map.insert(tmmap, n, mk_var(s, Vector.sub(tyv, tyn))))
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | stack_analysisLib.sml | 113 val r14 = mk_var("r14",``:word32``)
|
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
H A D | ho_discrimTools.sml | 83 val bv = mk_var (mk_string_fn bv_prefix [int_to_string (length bvs)], ty)
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
H A D | vars_as_resourceSyntax.sml | 405 fun string2num_var s = mk_var(s, numLib.num);
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | testTypesScript.sml | 322 val _ = save_thm("LIST",LIST_CONJ (map (REFL o curry mk_var "a")
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | bitstringScript.sml | 338 FAIL $' ^(Term.mk_var ("index too large", Type.bool)) 800 FAIL $word_join ^(Term.mk_var("bad domain", Type.bool)) 811 FAIL $word_concat ^(Term.mk_var("bad domain", Type.bool))
|
H A D | wordsLib.sml | 55 val Na = Term.mk_comb (numSyntax.numeral_tm, Term.mk_var ("a", numLib.num)) 799 then mk_var (" ", Term.type_of t) 990 val x = Term.variant fvs (Term.mk_var ("x", ty)) 991 val y = Term.variant fvs (Term.mk_var ("y", ty)) 1197 then Term.mk_var (" ", type_of t) 1441 sum_n (List.map (shift_n (Term.mk_var ("x", ty))) (num2list v)) 1711 then cnv (f (Term.mk_var ("w", ty)))
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/step/ |
H A D | x64_stepLib.sml | 990 val imm8_tm = combinSyntax.mk_I (Term.mk_var ("imm", w8)) 1001 mk_extract (Term.mk_var ("imm", wordsSyntax.mk_int_word_type n)) 1084 val v = Term.mk_var ("v", Term.type_of wv)
|
/seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/src/ |
H A D | decidable_separationLogicLib.sml | 33 val v = mk_var("XXXX", type_of t); 1330 val t = subst [mk_var("pfL",type_of pf) |-> pf, 1331 mk_var("c1",type_of c1) |-> c1, 1332 mk_var("f2",type_of f2) |-> f2, 1333 mk_var("sfL",type_of sf) |-> sf] product_term;
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_opsScript.sml | 1073 val th = SPEC (mk_var("r5",``:word32``)) th 1086 val th = SPEC (mk_var("r5",``:word32``)) th 1112 val th = SPEC (mk_var("r5",``:word32``)) th 1125 val th = SPEC (mk_var("r5",``:word32``)) th 1151 val th = SPEC (mk_var("r5",``:word32``)) th 1164 val th = SPEC (mk_var("r5",``:word32``)) th
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_codegenScript.sml | 1566 val th = INST [mk_var("imm8",``:word8``)|->``(n2w ^n):word8``] th 1618 val def = new_definition(func_name,mk_eq(mk_comb(mk_var(func_name,ty),in_out_vars),result)) 1622 val pre = new_definition(func_name ^ "_pre",mk_eq(mk_comb(mk_var(func_name ^ "_pre",ty),in_out_vars),pre_result)) 1687 |> subst [mk_var("inst",type_of inst)|->inst] 1688 |> subst [mk_var("pre",type_of pre)|->pre] 1689 |> subst [mk_var("def",type_of def)|->def]
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | normalForms.sml | 161 let val v' = variant avoid (mk_var ("v", type_of v)) 944 val v = variant (all_vars b) (mk_var ("v", ty)) 980 AVOID_SPEC_TAC (vsel, mk_var (v, type_of vsel)) THEN
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | Normal.sml | 181 val id = let val x = mk_var("x",alpha) in mk_abs(x,x) end
|
/seL4-l4v-10.1.1/HOL4/examples/fsub/ |
H A D | full_subtypingScript.sml | 466 val n = mk_var("n", numSyntax.num)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/step/ |
H A D | arm8_stepScript.sml | 293 val nzcv = Term.mk_var ("nzcv", ``:bool # bool # bool # bool``)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/prog/ |
H A D | mips_progLib.sml | 35 val st = Term.mk_var ("s", ``:mips_state``)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/prog/ |
H A D | riscv_progLib.sml | 37 val st = Term.mk_var ("s", ``:riscv_state``)
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Mutual.sml | 330 val v' = mk_var(nm, ty')
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | sumScript.sml | 490 lift=SOME(mk_var("sumSyntax.lift_sum",
|