Searched refs:mk_var (Results 1 - 25 of 368) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/1/theory_tests/
H A Dgithub115aScript.sml5 val v1 = mk_var("v", bool --> bool)
6 val v2 = mk_var("v", bool)
/seL4-l4v-10.1.1/HOL4/tools/Holmake/tests/multibuild/
H A DmultiLib.sml7 val v = mk_var("v" ^ Int.toString n, bool)
/seL4-l4v-10.1.1/HOL4/src/refute/
H A Dselftest.sml3 fun Va n = mk_var("va" ^ Int.toString n, bool)
4 fun Vb n = mk_var("vb" ^ Int.toString n, bool)
/seL4-l4v-10.1.1/graph-refine/
H A Dinst_logic.py17 from syntax import mk_var namespace
96 inp_eqs = [((mk_var (nm, typ), 'ASM_IN'), (mk_var (nm, typ), 'C_IN'))
98 inp_eqs += [((logic.mk_rodata (mk_var (nm, typ)), 'ASM_IN'),
100 out_eqs = [((mk_var (nm, typ), 'ASM_OUT'), (mk_var (nm, typ), 'C_OUT'))
102 out_eqs += [((logic.mk_rodata (mk_var (nm, typ)), 'ASM_OUT'),
140 [syntax.mk_var (reg, syntax.word32T) for reg in inp_regs]
142 + [syntax.mk_var (nm, typ) for (nm, typ) in bin_globs],
/seL4-l4v-10.1.1/HOL4/src/1/
H A DnewtypeTools.sml23 val x = mk_var("x", oldty) and y = mk_var("y", oldty)
37 val g = mk_var("g", newty) and h = mk_var("h", newty)
H A DPsyntax.sml8 val mk_var = Term.mk_var value
H A DBoundedRewrites.sml13 ADD_ASSUM (mk_comb(bounded_tm, mk_var(Int.toString n, bool))) th
/seL4-l4v-10.1.1/HOL4/src/boss/
H A Dbool_defsScript.sml5 val LET_def = new_definition("LET_def",mk_eq(mk_var("LET",type_of(lhs(concl LET_DEF))),rhs(concl LET_DEF)))
7 val literal_case_def = new_definition("literal_case_def",mk_eq(mk_var("literal_case",type_of(lhs(concl literal_case_DEF))),rhs(concl literal_case_DEF)))
9 val IN_def = new_definition("IN_def",mk_eq(mk_var("IN",type_of(lhs(concl IN_DEF))),rhs(concl IN_DEF)))
11 val TYPE_DEFINITION_def = new_definition("TYPE_DEFINITION_def",mk_eq(mk_var("TYPE_DEFINITION",type_of(lhs(concl TYPE_DEFINITION))),rhs(concl TYPE_DEFINITION)))
/seL4-l4v-10.1.1/HOL4/src/floating-point/
H A Dmachine_ieeeLib.sml36 val mode = Term.mk_var ("mode", rounding_ty)
51 val fp_to_float_var = Term.mk_var (fp_to_float, fp_ty --> float_ty)
52 val w = Term.mk_var ("w", fp_ty)
70 val float_to_fp_var = Term.mk_var (float_to_fp, float_ty --> fp_ty)
71 val x = Term.mk_var ("x", float_ty)
82 val fp_to_real_var = Term.mk_var (fp_to_real, fp_ty --> real_ty)
92 val fp_to_value_var = Term.mk_var (fp_to_value, fp_ty --> value_ty)
103 Term.mk_var (real_to_fp, rounding_ty --> real_ty --> fp_ty)
114 Term.mk_var
126 val a = Term.mk_var ("
[all...]
/seL4-l4v-10.1.1/HOL4/src/marker/
H A DmarkerSyntax.sml19 let val l = mk_var(s,type_of tm)
34 val v1 = mk_var(s1,type_of rhs1)
35 val v2 = mk_var(s2,type_of rhs2)
52 REFL(mk_var(fst(dest_var tm),mk_vartype "'abbrev"))
79 list_mk_comb(label_tm, [mk_var(s, label_ty), t]);
/seL4-l4v-10.1.1/HOL4/src/boss/ml_evaluation/
H A DLift.sml24 val list_mk_comb_var = mk_var("list_mk_comb", Type`:'term -> 'term`)
25 val cons_var = mk_var ("cons",Type`:'term -> 'term -> 'term`)
26 val nil_var = mk_var ("nil",Type`:'term`)
27 val comma_var = mk_var (",",Type`:'term -> 'term -> 'term`)
33 val argvs = map mk_var (zip (enum_list "v" (length argtys)) argtys)
43 in mk_var(cname,ty')
54 val flist = map mk_var (zip flistnames flist_types)
57 val lift_var = mk_var("lift",lift_type)
68 Pair (mk_var(Cname,termty))
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/decompiler/
H A Darm_core_decompLib.sml14 val r15 = Term.mk_var ("r15", ``:word32``)
26 val vars = Term.mk_var ("cond", Type.bool) ::
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/tools/
H A DcongToolsLib.sml37 val var = mk_var ("x", hol_type)
49 val var1 = mk_var ("x1", hol_type)
50 val var2 = mk_var ("x2", hol_type)
51 val var3 = mk_var ("x3", hol_type)
/seL4-l4v-10.1.1/HOL4/src/HolSat/
H A DsatCommonTools.sml24 val mk_var = Term.mk_var; value
48 val t = mk_var("t",bool)
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/Solitaire/
H A DHexSolitaireScript.sml80 if n<10 then mk_var("v0"^(int_to_string n),bool)
81 else mk_var("v"^(int_to_string n),bool);
84 if n<10 then mk_var("v0"^(int_to_string n)^"'",bool)
85 else mk_var("v"^(int_to_string n)^"'",bool);
93 fun mk_bool_var s = mk_var(s,bool);
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/examples/
H A Dltl2omega.sml46 | mpattern_int n = subst [mk_var ("X", ``:'a ltl``) |-> mpattern_int (n-1)]
49 fun mpattern n = subst [mk_var ("X", ``:'a ltl``) |-> mpattern_int n]
55 | bpattern n = subst [mk_var ("X", ``:'a ltl``) |-> bpattern (n-1)]
88 subst [mk_var ("X1", ``:'a ltl``) |-> x1_term,
89 mk_var ("X2", ``:'a ltl``) |-> x2_term] pattern
100 val term = subst [mk_var ("X1", ``:'a ltl``) |-> t1,
101 mk_var ("X2", ``:'a ltl``) |-> t2,
102 mk_var ("X3", ``:'a ltl``) |-> t3] pattern
106 val term = subst [mk_var ("m", ``:'a ltl``) |-> m,
107 mk_var ("
[all...]
/seL4-l4v-10.1.1/HOL4/src/patricia/
H A DpatriciaLib.sml274 val p = Term.mk_var ("p", numLib.num)
275 val m = Term.mk_var ("m", numLib.num)
276 val k = Term.mk_var ("k", numLib.num)
277 val j = Term.mk_var ("j", numLib.num)
295 val d = Term.mk_var ("d", tty)
296 val l = Term.mk_var ("l", ty)
297 val r = Term.mk_var ("r", ty)
384 val p = Term.mk_var ("p", numLib.num)
385 val m = Term.mk_var ("m", numLib.num)
386 val j = Term.mk_var ("
[all...]
/seL4-l4v-10.1.1/HOL4/src/proofman/tests/
H A Dselftest.sml31 val f = mk_var("f", alpha --> alpha)
32 val gg = mk_var("g", beta --> gamma --> alpha)
33 val g = mk_var("g", gamma --> alpha)
34 val x = mk_var("x", gamma)
35 val b = mk_var("b", beta)
100 val t = boolSyntax.list_mk_conj (map(fn s => mk_var(s,bool)) strings)
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/
H A Dtemporal_deep_simplificationsLib.sml51 val resultTerm = subst [mk_var("x", type_of t) |-> t,
52 mk_var("y", type_of t) |-> l,
53 mk_var("z", type_of t) |-> new_r] resultTerm
83 val resultTerm = subst [mk_var("x", type_of t) |-> t,
84 mk_var("y", type_of t) |-> l,
85 mk_var("z", type_of t) |-> new_r] resultTerm
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A Dstack_introLib.sml19 val th = th |> INST [m |-> mk_var("stack" ,type_of m),
20 d |-> mk_var("dom_stack" ,type_of d)]
44 val r13 = mk_var("r13",``:word32``)
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/arm/
H A Dprog_armLib.sml35 in (mk_comb(``aR``,tm),mk_var("r" ^ f tm,``:word32``)) end
36 else if tm = ``psrN:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrn",``:bool``))
37 else if tm = ``psrZ:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrz",``:bool``))
38 else if tm = ``psrC:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrc",``:bool``))
39 else if tm = ``psrV:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrv",``:bool``))
40 else if tm = ``psrQ:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrq",``:bool``))
42 (mk_comb(``aM1:word32 -> word8 -> arm_set -> bool``,tm),mk_var(name_of_tm tm,``:word8``))
46 val r15 = mk_var("r15",``:word32``)
53 val cpsr_var = mk_var("cpsr",``:word32``)
74 val code = subst [mk_var("
[all...]
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/
H A DibmLib.sml344 mk_var ("i0", num) |-> i0,
345 mk_var ("s0", num) |-> s0] i0_le_s0_term;
350 mk_var ("A", ``:num symbolic_semi_automaton``) |-> A,
351 mk_var ("i0", num) |-> i0,
352 mk_var ("s0", num) |-> s0] state_vars_term;
358 mk_var ("A", ``:num symbolic_semi_automaton``) |-> A,
359 mk_var ("s0", num) |-> s0] used_vars_term;
372 mk_var ("p", ``:num prop_logic``) |-> p,
373 mk_var ("s0", num) |-> s0] used_vars_term;
501 mk_var ("ps
[all...]
/seL4-l4v-10.1.1/HOL4/examples/countable/
H A Dcountable_initScript.sml61 val x = mk_var("x",ty)
62 val y = mk_var("y",ty)
H A DcountableLib.sml24 let val vs = Redblackmap.foldl (fn (n,ty,ls) => mk_var(n,ty)::ls) [] d
36 val v' = mk_var (Lib.prime n, ty)
43 val helpers = map (fn a => mk_var("count_"^(dest_vartype a),a --> num)) args
46 mk_var(count_name_aux,
71 val hyps = map (mk_inj_rwt_tm []) (zip (map (fn a => mk_var(dest_vartype a, a)) args) helpers)
/seL4-l4v-10.1.1/HOL4/src/num/theories/
H A DbasicSize.sml22 val lift_bool_var = mk_var("boolSyntax.lift_bool",ty --> bool --> tm)
50 val lift_one_var = mk_var("oneSyntax.lift_one", ty --> oneSyntax.one_ty --> tm)

Completed in 235 milliseconds

1234567891011>>