Searched refs:var (Results 76 - 100 of 283) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/mos-count/
H A Dtoplevel.ml68 else let var = fst (dest_forall (concl thm)) in
69 if not (type_of tm = type_of var) then ALL_TAC
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/
H A Dcppext.cxx98 BDD *var = NEW(BDD,width); local
104 var[n] = variables[n].root;
106 res = bdd_buildcube(val, width, var);
108 free(var);
186 void printhandler(ostream &o, int var)
189 o << names[var];
510 void printhandler(ostream &o, int var)
513 o << names[var];
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/
H A DvariableScript.sml58 val _ = Hol_datatype `var = VAR of string => num`;
91 (* RW_TAC std_ss (type_rws "var") (* or list_ss or arith_ss *) *)
171 new_infix("is_variant", ==`:var->var->bool`==, 450);
464 ���SUC(CARD (s:var -> bool))���] LESS_CASES)
535 THEN ASSUME_TAC (INST_TYPE[==`:'a`== |-> ==`:var`==] FINITE_EMPTY)
578 THEN EXISTS_TAC ���s:var -> bool���
681 THEN IMP_RES_THEN (ASSUME_TAC o SPEC ���x:var���) variant_THM
739 THEN EXISTS_TAC ���(y:var) INSERT s���
843 THEN (MP_TAC o SPECL[���x:(var)lis
[all...]
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/
H A DvariableScript.sml64 val _ = Hol_datatype `var = VAR of string => num`;
97 (* RW_TAC std_ss (type_rws "var") (* or list_ss or arith_ss *) *)
177 new_infix("is_variant", ==`:var->var->bool`==, 450);
470 ���SUC(CARD (s:var -> bool))���] LESS_CASES)
541 THEN ASSUME_TAC (INST_TYPE[==`:'a`== |-> ==`:var`==] FINITE_EMPTY)
584 THEN EXISTS_TAC ���s:var -> bool���
687 THEN IMP_RES_THEN (ASSUME_TAC o SPEC ���x:var���) variant_THM
745 THEN EXISTS_TAC ���(y:var) INSERT s���
849 THEN (MP_TAC o SPECL[���x:(var)lis
[all...]
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DcongLib.sml62 val var = mk_var ("x", hol_type) value
64 val reflThm = refl {Rinst=preorderTerm,arg=var}
75 val var = mk_var ("x", hol_type) value
77 val reflThm = refl {Rinst=preorderTerm,arg=var}
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/
H A DwpTools.sml103 val var = genvar (type_of wlp_post) value
104 val query = mk_leq (var, wlp_post)
105 val result = hd (snd (vc_solve (([var],[]),[query])))
123 val _ = is_var la orelse raise ERR "dest_lam" "lhs rator not var"
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DThm.sig74 val freeIn : Term.var -> thm -> bool
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DThm.sig74 val freeIn : Term.var -> thm -> bool
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dprog_x86Lib.sml43 val var = mk_var(name_for_resource x name, type_of pattern) value
44 in mk_eq(subst [lhs |-> name] pattern,var) end
71 fun mk_pre_post_assertion (name,var) = let
77 else if type_of var = ``:word8`` then
79 else if type_of var = ``:word32`` then
81 in (subst [name_tm|->name,var_tm|->var] pattern,
82 subst [name_tm|->name,var_tm|->get_assigned_value name var] pattern) end
/seL4-l4v-10.1.1/HOL4/src/lite/
H A DliteLib.sml417 fun MK_ABS_CONV var tm =
418 if (Term.is_comb tm andalso (Term.rand tm = var)
419 andalso not (Term.free_in var (Term.rator tm)))
422 let val rhs = Term.mk_abs(var,tm)
423 val newrhs = Term.mk_comb(rhs,var)
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DtestTypesScript.sml241 var = VAR of String;
248 val _ = AddType `:var`;
269 | VARatpat_e of var
281 | LAYEREDpat_e of var => pat_e;
291 | VARatexp_e of var long
/seL4-l4v-10.1.1/HOL4/src/temporal/src/
H A DtemporalLib.sml41 var of string |
102 in var(n)
178 | temporal2hol (var(x)) = mk_var{Name=x,Ty=(==`:num->bool`==)}
274 | var_names (var(x)) = [x]
328 | var(n) => var(n)
383 var(_) => ([],Phi)
421 val ell0 = var(ell0_name)
422 val ell1 = var(ell1_name)
432 val ell = var(ell_nam
[all...]
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/
H A DmodelCheckLib.sml255 if (((bdd.hash (bdd.high b) = 1) andalso (bdd.hash (bdd.low b) = 0))) then (num_to_var_string (bdd.var b)) else
256 if (((bdd.hash (bdd.high b) = 0) andalso (bdd.hash (bdd.low b) = 1))) then ("!"^(num_to_var_string (bdd.var b))) else
267 val var_s = num_to_var_string (bdd.var b);
270 ("("^(num_to_var_string (bdd.var b))^" | "^bdd_to_definition (low b)^")") else
272 ("(!"^(num_to_var_string (bdd.var b))^" | "^bdd_to_definition (high b)^")") else
274 ("(!"^(num_to_var_string (bdd.var b))^" & "^bdd_to_definition (low b)^")") else
276 ("("^(num_to_var_string (bdd.var b))^" & "^bdd_to_definition (high b)^")") else
484 fun varrenaming_foldr ((term, var), s) =
486 val x = "x"^(int_to_string var);
/seL4-l4v-10.1.1/HOL4/src/new-datatype/
H A DNDatatype.sml337 val var = genvar ty value
338 in [(var, f var)]
342 val var = genvar a value
343 val inv = sumSyntax.mk_inl(var, b)
345 in (var, inv)::(div_sum_vars b f' (n-1))
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/concurrent/
H A DTask_Queue.sml62 status: exn option Synchronized.var}
67 fun new_group parent = make_group (parent, new_id (), Synchronized.var "group_status" NONE);
109 else SOME (Synchronized.var "timing" timing_start);
116 timing: timing Synchronized.var option}
140 val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t));
/seL4-l4v-10.1.1/HOL4/examples/lambda/basics/
H A Dgeneric_termsScript.sml21 pregterm = var string 'v
26 (fv (var s vv) = {s}) ���
36 (���s vv. P (var s vv)) ���
54 (raw_ptpm p (var s vv) = var (lswapstr p s) vv) ���
116 (allatoms (var s vv) = {s}) ���
171 (!s vv. aeq (var s vv) (var s vv)) /\
185 ``~aeq (var s vv) (lam v bv ts us)``,
268 ``aeq (var v
[all...]
/seL4-l4v-10.1.1/HOL4/examples/CCS/
H A DCCSScript.sml285 | var 'a
348 (CCS_Subst (var Y) E' X = if (Y = X) then E' else (var Y)) /\
363 (* |- ���X E. CCS_Subst (var X) E X = E (2nd fixed point of CCS_Subst) *)
366 (REWRITE_CONV [CCS_Subst_def] ``CCS_Subst (var X) E X``));
451 |- !X u E'. ~TRANS (var X) u E'
456 (Q.SPECL [`var X`, `u`, `E`] TRANS_cases)));
828 (FV (var X) = {X}) /\
839 (BV (var X) = EMPTY) /\
859 (CCS_Subst1 (var
[all...]
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/
H A DPrimitiveBddRules.sml256 (* replace b (makepairSet[(var b1, var b1'), ... , (var bi, var bi')]) *)
285 ((bdd.var b, bdd.var b')::replacel)))
331 (* (subst [v |-> tm1] tm2) |--> compose (var b, b1) b2 *)
344 bdd.compose (bdd.var b, b1) b2)
359 (* veccompose (composeSet (map (var ## I) [(b1,b1'), ... , (bi,bi')])) b *)
382 ((bdd.var
[all...]
/seL4-l4v-10.1.1/HOL4/src/HolQbf/
H A DQbfCertificate.sml171 datatype vtype = Forall of term (* var *)
172 | Exists of (term * term) (* var, extvar *)
220 val (var,lits',deps) = value
231 in enum (insert(vars,vi,var)) t lits' deps (SOME vi) end
374 val var_dict = List.foldl (fn ((i, var, is_forall), var_dict) =>
375 Redblackmap.insert (var_dict, var, (i, is_forall)))
377 fun index_fn var =
378 Redblackmap.find (var_dict, var)
/seL4-l4v-10.1.1/HOL4/src/HolSat/
H A DminisatResolve.sml16 (*+1 because minisat var numbers start at 0,SatLib at 1*)
78 where v is the only var that occurs with opposite signs in c0 and c1 *)
/seL4-l4v-10.1.1/HOL4/src/real/
H A DDiff.sml107 val var = variant (frees tm) lreal value
108 val tm2 = mk_comb(tm1,var)
/seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/
H A DswapScript.sml450 (!s p. rFV (var s p) SUBSET (s INSERT pFV p UNION X)) /\
462 (rswap x y (var s p) = var (swapstr x y s) (pswap x y p))) /\
476 (!s p. hom (VAR s) p = var s p) /\
631 Q.INST [`var'` |-> `var`, `con'` |-> `con`, `app'` |-> `app`,
635 `var` |-> `\s p. var' s`,
/seL4-l4v-10.1.1/HOL4/src/compute/examples/
H A DArith.sml39 * strongly (arg of a free var), but we will have to reduce the
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DSup_Inf.sml66 fun solve_ineqs ineqs var =
70 and (restl,restr) = solve_ineqs (tl ineqs) var
71 in (let val i = assoc var bind
74 (filter (fn (name,_) => not (name = var)) bind)
/seL4-l4v-10.1.1/HOL4/examples/muddy/
H A Dbvec.sml16 val var: precision -> varnum -> int -> bvec = app3 (symb "mlbvec_var") value

Completed in 307 milliseconds

1234567891011>>