/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/step/ |
H A D | riscv_stepLib.sml | 29 val x = Term.mk_var ("x", wordsSyntax.mk_int_word_type 32)
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Pmatch.sml | 54 fn ty => mk_var(pass "v", ty) 488 of VAR v => [mk_var v] 733 val f = if is_var f0 then f0 else mk_var(dest_const f0) 737 val a = variant avs (mk_var("a", type_of(Lib.trye hd pats)))
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/ |
H A D | dpll.sml | 148 fun mk_index s i = mk_var(s ^ "_" ^ Int.toString i, bool)
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | posetScript.sml | 42 val v = mk_var (unprime sp, ty)
|
H A D | PairedLambda.sml | 66 val xv = mk_var("x", type_of varstruct)
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | matchTools.sml | 220 fun g v (_, y) = v |-> mk_var (y, type_of v)
|
H A D | folTools.sml | 583 fun h v = Term.mk_var (v, Type.alpha); 590 val f' = Term.mk_var (f,ty)
|
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibAbbrev.sml | 101 val new_v = variant (!fvL) (mk_var (ss, type_of st))
|
/seL4-l4v-10.1.1/HOL4/src/real/ |
H A D | hrealScript.sml | 566 DISCH_THEN(EVERY_TCL (map (X_CHOOSE_THEN o C (curry mk_var) (==`:hrat`==)) 581 DISCH_THEN(EVERY_TCL (map (X_CHOOSE_THEN o C (curry mk_var) (==`:hrat`==)) 598 [DISCH_THEN(EVERY_TCL (map (X_CHOOSE_THEN o C (curry mk_var) (==`:hrat`==)) 603 DISCH_THEN(EVERY_TCL (map (X_CHOOSE_THEN o C (curry mk_var) (==`:hrat`==))
|
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
H A D | wpTools.sml | 56 (variant (free_varsl (g :: asl))) (mk_var (n, type_of t))
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootSyntax.sml | 78 val var_term = variant (free_vars term) (mk_var (var, Type `:holfoot_var`));
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/examples/ |
H A D | ibm.sml | 212 val var = mk_var (s, type_of replace);
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/Solitaire/ |
H A D | SolitaireScript.sml | 71 fun mk_bool_var s = mk_var(s,bool)
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | envTools.sml | 44 in fun get_env_val state q e = get_env_val_aux (mk_abs(mk_var("q",``:string``),mk_pabs(state,F))) q e end
|
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/ |
H A D | Term.sml | 118 val mk_var = Var value 122 in mk_var(spin Name, Ty) 620 val new_v = mk_var (new_vname, vty) 843 in mk_var(loop Name, Ty) 859 val newvar0 = mk_var(newname, ty)
|
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | ListConv1.sml | 490 val ev = Term.mk_var ("e", ety) 491 val xv = Term.mk_var ("x", lty) 492 val lv = Term.mk_var ("l", Term.type_of l) 494 ([Term.mk_var ("f", Term.type_of f) |-> f], 1255 val nv = mk_var{Name="n",Ty=(==`:num`==)}
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/step/ |
H A D | m0_stepLib.sml | 38 val st = Term.mk_var ("s", Type.mk_type ("m0_state", [])) 651 val f_tm = Term.mk_var ("f", Term.type_of ``m0_step$R_name b``) 652 val b_tm = Term.mk_var ("b", wordsSyntax.mk_int_word_type 32) 653 val r_tm = Term.mk_var ("r", ``:RName -> word32``) 654 val m_tm = Term.mk_var ("r", ``:word32 -> word8``) 1329 (n, fn i => Term.mk_var ("x" ^ Int.toString (i + p), Type.bool) |->
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | syntax.py | 767 return mk_var (renames[expr.name], expr.typ) 1312 def mk_var (nm, typ): function 1485 mks = (mk_var, mk_plus, mk_uminus, mk_minus, mk_times, mk_modulus, mk_bwand,
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/prog/ |
H A D | arm8_progLib.sml | 28 val pc_tm = Term.mk_var ("pc", dword) 213 val st = Term.mk_var ("s", ``:arm8_state``)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/step/ |
H A D | arm8_stepLib.sml | 38 fun reg_var v = Term.mk_var (v, reg_ty) 305 fun mk_sz i = Term.mk_var ("sz", wordsSyntax.mk_int_word_type i)
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | fcpScript.sml | 807 FAIL (fcp_index) ^(mk_var("index out of range", bool)) ((a :+ w) m) b`, 915 FAIL $' ^(mk_var("FCP out of bounds", bool))
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | HolKernel.sml | 505 in fn ty => mk_var (name, ty) 606 mk_var (xn, type_subst (#1 tyins) xty)
|
/seL4-l4v-10.1.1/HOL4/examples/fsub/ |
H A D | kernel_subtypingScript.sml | 151 val n = mk_var("n", numSyntax.num)
|
/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | Term.sml | 308 val mk_var = Fv value 315 in mk_var(spin Name, Ty) 359 in mk_var(loop Name, Ty) 753 val v' = mk_var(n',ty)
|
/seL4-l4v-10.1.1/HOL4/src/enumfset/ |
H A D | totoTacs.sml | 71 val var1 = mk_var ("_z", Type`:bool`); (* supposedly not an identifier *)
|