Searched refs:var (Results 51 - 75 of 283) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/portableML/poly/
H A DStandard_Thread.sml30 val name_var = Thread_Data.var () : string Thread_Data.var;
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/
H A DholfootSyntax.sml71 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 DMakefile71 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 DSolve_ineqs.sml297 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 DSol_ranges.sml164 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 DUnwind.sml80 * 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 Dexample.sml18 type_spec =`var = VAR of string`};
20 val var_ty = Parse.Type`:var`;
25 atexp ::= <var>
46 | <var>
H A Dvar_example.sml8 val var_ty = (==`:'var`==)
80 (--`(atexpV (var_exp (v:'var)) = {v}) /\
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/
H A Dcplex.py110 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 Dkernel.c861 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 Dbddio.c79 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 Dsvmono.cls644 % the upright forms are defined here as \var<Character>
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Prog_Prove/document/
H A Dsvmono.cls644 % the upright forms are defined here as \var<Character>
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DProof.sig45 val freeIn : Term.var -> proof -> bool
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DProof.sig45 val freeIn : Term.var -> proof -> bool
/seL4-l4v-10.1.1/HOL4/examples/muddy/
H A Dbvec.sig10 val var: fdd.precision -> bdd.varnum -> int -> bvec value
68 var bvec_var
H A Dbdd.sml81 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 DcongToolsLib.sml37 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 DalphaScript.sml32 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 DncScript.sml185 !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 DStrongLawsScript.sml1173 |- ���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 Dsolver.py362 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 DSmtLib_Parser.sml202 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 Dres_quanLib.sml112 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 DNormal.sml78 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 *)

Completed in 292 milliseconds

1234567891011>>