/seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
H A D | Standard_Thread.sml | 30 val name_var = Thread_Data.var () : string Thread_Data.var;
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootSyntax.sml | 71 val var = "x"; 75 fun holfoot_mk_var_abs (var, term) = 77 val sm_var_term = string2holfoot_var var; 78 val var_term = variant (free_vars term) (mk_var (var, Type `:holfoot_var`)); 86 fun holfoot_mk_local_var (var,term) = 87 mk_icomb (var_res_prog_local_var_term, holfoot_mk_var_abs (var, term)); 89 fun holfoot_mk_call_by_value_arg ((var,expr),term) = 90 list_mk_icomb (var_res_prog_call_by_value_arg_term, [holfoot_mk_var_abs (var, term), expr]);
|
/seL4-l4v-10.1.1/l4v/tools/c-parser/standalone-parser/ |
H A D | Makefile | 71 ARM_MLB_PATH := -mlb-path-var 'L4V_ARCH ARM' 72 ARM_HYP_MLB_PATH := -mlb-path-var 'L4V_ARCH ARM_HYP' 73 X64_MLB_PATH := -mlb-path-var 'L4V_ARCH X64' 74 RISCV64_MLB_PATH := -mlb-path-var 'L4V_ARCH RISCV64'
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | Solve_ineqs.sml | 297 fun left_ineqs var icoeffsl = 300 (fn (name,coeff) => (name = var) andalso (coeff < zero)) 304 fun right_ineqs var icoeffsl = 307 (fn (name,coeff) => (name = var) andalso (coeff > zero)) 311 fun no_var_ineqs var icoeffsl = 315 (fn (name,coeff) => (name = var) andalso (not (coeff = zero))) 327 fun weighted_sums var pairs = 330 else let val (success,rest) = weighted_sums var (tl pairs) 335 WEIGHTED_SUM var (lcoeffs,rcoeffs) 352 val var value [all...] |
H A D | Sol_ranges.sml | 164 val var = hd vars value 165 val b = Bound (rat_zero,[(var,rat_one)]) 170 inst_var_in_coeffs (var,value) coeffsl' 171 in (var,value)::(Shostak' new_coeffsl (tl vars))
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Unwind.sml | 80 * Given a quantified variable $var$, and a list of possible restricting 82 * a conjunct from the list of the form $(var = val)$ or $(val = var)$ 83 * or $var$ or $~var$. 96 fun check_var var conj = 102 if (arg1 = var) then arg2 else 103 if (arg2 = var) then arg1 105 else if is_neg conj andalso dest_neg conj = var then false_tm 106 else if var [all...] |
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/examples/ |
H A D | example.sml | 18 type_spec =`var = VAR of string`}; 20 val var_ty = Parse.Type`:var`; 25 atexp ::= <var> 46 | <var>
|
H A D | var_example.sml | 8 val var_ty = (==`:'var`==) 80 (--`(atexpV (var_exp (v:'var)) = {v}) /\
|
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
H A D | cplex.py | 110 for (i,var) in enumerate(var_s): 113 tmp_f.write("1 %s"% var)
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | kernel.c | 861 PROTO {* BDD bdd_ithvar(int var) *} 869 the index {\tt var} that also defines the position in the 874 BDD bdd_ithvar(int var) argument 876 if (var < 0 || var >= bddvarnum) 882 return bddvarset[var*2]; 890 PROTO {* BDD bdd_nithvar(int var) *} 900 BDD bdd_nithvar(int var) argument 902 if (var < 0 || var > [all...] |
H A D | bddio.c | 79 void printhandler(FILE *o, int var) 82 fprintf(o, "%s", names[var]); 542 int key,var,low,high,root=0,n; local 546 if (fscanf(ifile,"%d %d %d %d", &key, &var, &low, &high) != 4) 554 if (low<0 || high<0 || var<0) 557 root = bdd_addref( bdd_ite(bdd_ithvar(var), high, low) );
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Prog_Prove/document/ |
H A D | svmono.cls | 644 % the upright forms are defined here as \var<Character>
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Prog_Prove/document/ |
H A D | svmono.cls | 644 % the upright forms are defined here as \var<Character>
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Proof.sig | 45 val freeIn : Term.var -> proof -> bool
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Proof.sig | 45 val freeIn : Term.var -> proof -> bool
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/ |
H A D | bvec.sig | 10 val var: fdd.precision -> bdd.varnum -> int -> bvec value 68 var bvec_var
|
H A D | bdd.sml | 81 val var : bdd -> varnum = app1 (symb "mlbdd_bdd_var") value 192 else let val var = var bdd value 195 in if equal low FALSE then loop high ((var,true) :: acc) 196 else loop low ((var,false) :: acc) 244 in update root (var r,
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/tools/ |
H A D | congToolsLib.sml | 37 val var = mk_var ("x", hol_type) value 39 val reflThm = refl {Rinst=preorderTerm,arg=var}
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/ |
H A D | alphaScript.sml | 32 val vars = ty_antiq( ==`:var list`== ); 33 val subs1 = ty_antiq( ==`:(var # obj1) list`== ); 49 ` obj1 = OVAR1 of var 56 method1 = SIGMA1 of var => obj1 ` ; 70 (alpha_match (CONS (x:var) xs) ys x1 y1 = 102 EXT_TAC ���x:var��� 104 THEN EXT_TAC ���y:var��� 501 [ UNDISCH_THEN���(y:var) = x'��� REWRITE_ALL_THM 504 THEN EXISTS_TAC ���x:var��� 505 THEN EXISTS_TAC ���y':var��� [all...] |
/seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/ |
H A D | ncScript.sml | 185 !var : string->'b. 190 (!x. hom(VAR x) = var x) /\ 194 THEN Q.EXISTS_TAC `\x. HOM (con:'a ->'b) var lam app (REP_nc x)` 201 !var : string->'b. 206 (!x. hom(VAR x) = var x) /\ 355 and var = Term`\s:string. (VAR s:'a nc, (var s:'b) )` value 361 val th1 = SPECL [con,var,app,lam] instth 378 (!x. SND p(VAR x) = var x) /\ 392 var [all...] |
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | StrongLawsScript.sml | 1173 |- ���u s v. u..rec s (v..u..var s) ~ rec s (u..v..var s): 1178 STRONG_EQUIV (prefix u (rec s (prefix v (prefix u (var s))))) 1179 (rec s (prefix u (prefix v (var s))))``, 1185 (x = prefix u' (rec s' (prefix v' (prefix u' (var s'))))) /\ 1186 (y = rec s' (prefix u' (prefix v' (var s')))) \/ 1187 (x = rec s' (prefix v' (prefix u' (var s')))) /\ 1188 (y = prefix v' (rec s' (prefix u' (prefix v' (var s')))))`` 1200 [ASSUME ``E = prefix u' (rec s' (prefix v' (prefix u' (var s'))))``] 1203 EXISTS_TAC ``prefix (v' :'b Action) (rec s' (prefix u' (prefix v' (var [all...] |
/seL4-l4v-10.1.1/graph-refine/ |
H A D | solver.py | 362 var = solv.add_pvalids (htd_s, typ, p_s, expr.name) 363 return var 418 var = solv.add_var ('updated_htd', expr.typ) 419 return var 439 var = solv.add_var ('invented', expr.typ) 440 return var 932 trace ('WARNING: redef of var %r to name %s' % (val, name)) 1424 v = self.add_var ('arbitary-var', typ, kind = 'Aux') 1688 var = self.add_pvalids (htd_s, ('Type', r_typ), 1691 self.assert_fact_smt (var) [all...] |
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | SmtLib_Parser.sml | 202 fun parsefn var token nums args = 204 var 206 raise ERR ("<" ^ Hol_pp.term_to_string var ^ ">") 209 (List.map (fn (s, var, _) => (s, parsefn var)) bindings) 213 pairSyntax.mk_anylet (List.map (fn (_, var, t) => (var, t)) bindings, body) 244 fun parsefn var token nums args = 246 var 248 raise ERR ("<" ^ Hol_pp.term_to_string var [all...] |
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/ |
H A D | res_quanLib.sml | 112 val (var, a) = dest_forall tm value 116 if not(var = v) 119 SYM (RIGHT_CONV_RULE ((GEN_ALPHA_CONV var) THENC 121 (ISPECL [pred,mk_abs(var,t)] dthm)) 134 val (var,pred,conj) = dest_res_forall tm value 136 val left_pred = mk_abs(var,left) 137 val right_pred = mk_abs(var,right) 480 <varstruct> ::= <var> | (<varstruct>,...,<varstruct>) 502 <lhs> ::= <var> | <lhs> <varstruct> 521 else raise ERR "check_lhs" "var use [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | Normal.sml | 78 else (* const op var *) 82 (if is_8bit_literal d1 then (* var op const *) 84 else (* var op var *) 256 else (* const op var *) 259 else (* var op const || var op var *)
|