Searched refs:var (Results 1 - 25 of 283) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/
H A Dprotoparamshadow.c11 int var; variable
13 int proto(int var);
15 int realone(int var) argument
17 return var + 1;
22 var = var + 1;
23 return var;
26 int var = 4; variable
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/
H A DSynchronized.sml9 type 'a var
10 val var: string -> 'a -> 'a var value
11 val value: 'a var -> 'a
12 val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
13 val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
14 val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
15 val change: 'a var -> ('a -> 'a) -> unit
23 abstype 'a var = Var of
27 var
30 fun var name x = Var function
[all...]
H A DSingle_Assignment.sml9 type 'a var
10 val var: string -> 'a var value
11 val peek: 'a var -> 'a option
12 val await: 'a var -> 'a
13 val assign: 'a var -> 'a -> unit
19 abstype 'a var = Var of
23 var: 'a SingleAssignment.saref}
26 fun var name = Var function
30 var
[all...]
H A DThread_Data.sml9 type 'a var
10 val var: unit -> 'a var value
11 val get: 'a var -> 'a option
12 val put: 'a var -> 'a option -> unit
13 val setmp: 'a var -> 'a option -> ('b -> 'c) -> 'b -> 'c
20 abstype 'a var = Var of 'a option Universal.tag
23 fun var () : 'a var = Var (Universal.tag ()); function
H A DCounter.sml19 val counter = Synchronized.var "counter" 0;
/seL4-l4v-10.1.1/HOL4/Manual/Quick/
H A Dquick.tex15 \newcommand{\var}[1]{{\emph{#1}}}
27 \hol{Theory}{new_theory} \var{name} & creates a new theory\\
29 \hol{TotalDefn}{Define} \var{term} & function definition \\
30 \hol{bossLib}{Hol_datatype} \var{type-dec} & defines a concrete datatype \\
31 \holnoref{EquivType}{define_equivalence_type} \var{rec} & type of equivalence classes \\
32 \hol{Theory}{save_thm}(\var{name},\var{thm}) & stores theorem \\
33 \hol{Tactical}{prove}(\var{term},\var{tactic}) & proves theorem using tactic \\
34 \hol{Tactical}{store_thm}(\var{nam
[all...]
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/
H A Dfdd.h87 inline bdd fdd_ithvarpp(int var, int val) argument
88 { return fdd_ithvar(var, val); }
90 inline bdd fdd_ithsetpp(int var) argument
91 { return fdd_ithset(var); }
93 inline bdd fdd_domainpp(int var) argument
94 { return fdd_domain(var); }
96 inline int fdd_scanvar(const bdd &r, int var) argument
97 { return fdd_scanvar(r.root, var); }
118 inline bdd* fdd_conpp(int bitnum, int var)
119 { return fdd_transfer( bitnum, fdd_con(bitnum, var) ); }
[all...]
H A Dfdd.c57 BDD var; /* The BDD variable set */ member in struct:s_Domain
178 domain[n+fdvarnum].var = bdd_makeset(domain[n+fdvarnum].ivar,
180 bdd_addref(domain[n+fdvarnum].var);
237 d->var = bdd_makeset(d->ivar, d->binsize);
238 bdd_addref(d->var);
287 PROTO {* int fdd_domainsize(int var) *}
289 block {\tt var}. *}
308 PROTO {* int fdd_varnum(int var) *}
310 block {\tt var}. *}
329 PROTO {* int *fdd_vars(int var) *}
377 fdd_ithvar(int var, int val) argument
429 fdd_scanvar(BDD r, int var) argument
522 fdd_ithset(int var) argument
551 fdd_domain(int var) argument
737 int *var; local
1057 fdddec2bin(int var, int val) argument
[all...]
H A Dbddop.c96 static int replacelast; /* Current last var. level to replace */
147 #define RESTRHASH(r,var) (PAIR(r,var))
310 PROTO {* BDD bdd_buildcube(int value, int width, BDD *var)
311 BDD bdd_ibuildcube(int value, int width, int *var)*}
313 var}. It does so by interpreting the {\tt width} low order
317 the first variables in {\tt var}. Consider as an example
318 the call {\tt bdd\_buildcube(0xB, 4, var)}. This corresponds
319 to the expression: $var[0] \conj \neg var[
896 bdd_restrict(BDD r, BDD var) argument
1231 bdd_compose(BDD f, BDD g, int var) argument
1541 bdd_exist(BDD r, BDD var) argument
1592 bdd_forall(BDD r, BDD var) argument
1646 bdd_unique(BDD r, BDD var) argument
1745 bdd_appex(BDD l, BDD r, int opr, BDD var) argument
1811 bdd_appall(BDD l, BDD r, int opr, BDD var) argument
1877 bdd_appuni(BDD l, BDD r, int opr, BDD var) argument
2203 bdd_satoneset(BDD r, BDD var, BDD pol) argument
2229 satoneset_rec(BDD r, BDD var) argument
[all...]
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/
H A DSolver.C94 if (proof != NULL) proof->resolve(unit_id[var(qs[i])], var(qs[i]));
107 unit_id[var(ps[0])] = (sign(ps[0])) ? -id : id; //HA: sign info
118 int max = level[var(ps[1])];
120 if (level[var(ps[i])] > max)
121 max = level[var(ps[i])],
216 Var x = var(trail[c]);
251 bool operator () (Lit p, Lit q) { return trail_pos[var(p)] > trail_pos[var(q)]; }
276 if (!seen[var(
[all...]
H A DSolverTypes.h44 explicit Lit(Var var, bool sgn = false) : x((var+var) + (int)sgn) {} argument
48 friend int var (Lit p);
61 inline int var (Lit p) { return p.x >> 1; } function
72 inline int toDimacs(Lit p) { return sign(p) ? -var(p) - 1 : var(p) + 1; }
/seL4-l4v-10.1.1/HOL4/examples/CCS/
H A Dselftest.sml72 (``rec "VM" (In "coin"..(In "ask-esp"..rec "VM1" (Out "esp-coffee"..var "VM") +
73 In "ask-am"..rec "VM2" (Out "am-coffee"..var "VM")))``,
78 (In "ask-esp"..rec "VM1" (Out "esp-coffee"..var "VM") +
79 In "ask-am"..rec "VM2" (Out "am-coffee"..var "VM")))
92 (In "ask-esp"..rec "VM1" (Out "esp-coffee"..var "VM") +
93 In "ask-am"..rec "VM2" (Out "am-coffee"..var "VM")))) +
102 (In "ask-esp"..rec "VM1" (Out "esp-coffee"..var "VM") +
103 In "ask-am"..rec "VM2" (Out "am-coffee"..var "VM")))))���)];
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/
H A Dproblem-set-1-answers.lisp560 (defun boundp (var alist)
563 (if (equal var (car (car alist)))
565 (boundp var (cdr alist)))))
574 (defun binding (var alist)
577 (if (equal var (car (car alist)))
579 (binding var (cdr alist)))))
591 (defun bind (var val alist)
593 (cons (cons var (cons val nil)) nil)
594 (if (equal var (car (car alist)))
595 (cons (cons var (con
[all...]
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DSubst.sig25 val peek : subst -> Term.var -> Term.term option
27 val insert : subst -> Term.var * Term.term -> subst
29 val singleton : Term.var * Term.term -> subst
31 val toList : subst -> (Term.var * Term.term) list
33 val fromList : (Term.var * Term.term) list -> subst
35 val foldl : (Term.var * Term.term * 'a -> 'a) -> 'a -> subst -> 'a
37 val foldr : (Term.var * Term.term * 'a -> 'a) -> 'a -> subst -> 'a
H A DFormula.sig22 | Forall of Term.var * formula
23 | Exists of Term.var * formula
93 val destForall : formula -> Term.var * formula
97 val listMkForall : Term.var list * formula -> formula
101 val stripForall : formula -> Term.var list * formula
105 val destExists : formula -> Term.var * formula
109 val listMkExists : Term.var list * formula -> formula
113 val stripExists : formula -> Term.var list * formula
133 val freeIn : Term.var -> formula -> bool
H A DTerm.sig13 type var = Name.name type
22 Var of var
31 val destVar : term -> var
35 val equalVar : var -> term -> bool
107 val freeIn : var -> term -> bool
121 val variantPrime : NameSet.set -> var -> var
123 val variantNum : NameSet.set -> var -> var
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DSubst.sig25 val peek : subst -> Term.var -> Term.term option
27 val insert : subst -> Term.var * Term.term -> subst
29 val singleton : Term.var * Term.term -> subst
31 val toList : subst -> (Term.var * Term.term) list
33 val fromList : (Term.var * Term.term) list -> subst
35 val foldl : (Term.var * Term.term * 'a -> 'a) -> 'a -> subst -> 'a
37 val foldr : (Term.var * Term.term * 'a -> 'a) -> 'a -> subst -> 'a
H A DFormula.sig22 | Forall of Term.var * formula
23 | Exists of Term.var * formula
93 val destForall : formula -> Term.var * formula
97 val listMkForall : Term.var list * formula -> formula
101 val stripForall : formula -> Term.var list * formula
105 val destExists : formula -> Term.var * formula
109 val listMkExists : Term.var list * formula -> formula
113 val stripExists : formula -> Term.var list * formula
133 val freeIn : Term.var -> formula -> bool
H A DTerm.sig13 type var = Name.name type
22 Var of var
31 val destVar : term -> var
35 val equalVar : var -> term -> bool
107 val freeIn : var -> term -> bool
121 val variantPrime : NameSet.set -> var -> var
123 val variantNum : NameSet.set -> var -> var
/seL4-l4v-10.1.1/HOL4/src/HolQbf/
H A DQbfLibrary.sml53 val ((var, body), is_forall) = (boolSyntax.dest_forall t, true) value
58 (next_index + 1, (next_index, var, is_forall) :: vars, body)
93 (* 'CLAUSE_TO_SEQUENT'. Returns a list of triples ([~]i, [~]var, q), *)
138 val var = boolSyntax.dest_neg lit value
140 Thm.MP (Thm.INST [{redex = var, residue = boolSyntax.F}]
150 (* ----------------- bind_var hyp var true *)
151 (* A, !var. hyp |- t *)
154 (* ----------------- bind_var hyp var false (var not free in A or t) *)
155 (* A, ?var
[all...]
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/
H A DliftScript.sml33 val vars = ty_antiq( ==`:var list`== );
34 val subs = ty_antiq( ==`:(var # obj1) list`== );
70 ``:(var # obj1) list``;
333 ���!s1:^subs s2 t1 t2 (t:var -> bool).
370 THEN IMP_RES_TAC (MATCH_MP FST_RSP (identity_quotient (==`:var`==))),
409 [ EXISTS_TAC ���x':var���
414 EXISTS_TAC ���x':var���
651 (* !(var : var->'a) obj inv upd cns nil par sgm. *)
656 (* (!x. ho (OVAR1 x) = var
[all...]
/seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/
H A DlnamelessScript.sml23 val _ = Datatype`lnt = var string | bnd num | app lnt lnt | abs lnt`;
27 (open k u (var s) = var s) /\
34 (raw_lnpm pi (var s) = var (lswapstr pi s)) /\
64 (fv (var s) = {s}) /\
86 (!s. lclosed (var s)) /\
88 (!s t. ~(s IN fv t) /\ lclosed (open 0 (var s) t) ==>
102 (!s c. P (var s) c) /\
105 (!d. P (open 0 (var
[all...]
H A Draw_syntaxScript.sml52 val _ = Hol_datatype `raw_term = var of string
57 (fv (var s) = {s}) /\
68 (capt x (var y) = {}) /\
87 (subst x y (var s) = if y = s then x else var s) /\
95 ialpha y (lam x e) (lam y (subst (var y) x e))) /\
113 ``!e x. subst (var x) x e = e``,
143 ``!e x y. ~(y IN fv e) ==> (subst (var x) y (subst (var y) x e) = e)``,
148 (collapse (var
[all...]
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/
H A DliftScript.sml48 val subs = ty_antiq (``:(var # 'a term1) list``);
101 val ty = ``:(var # 'a term1) list``;
105 ``:(var # 'a term1) list``;
201 ���!s1:^subs s2 (t:var -> bool).
227 ���!s1:^subs s2 t1 t2 (t:var -> bool).
262 THEN IMP_RES_TAC (MATCH_MP FST_RSP (identity_quotient (==`:var`==))),
311 [ EXISTS_TAC ���x':var���
316 EXISTS_TAC ���x':var���
465 THEN EXISTS_TAC ���v:var���
478 THEN EXISTS_TAC ���v:var���
[all...]
/seL4-l4v-10.1.1/HOL4/src/datatype/record/
H A DRecordType.sml208 val var = Psyntax.mk_var(app_letter typ, typ) value
310 val f = gen_var_domty("f", fupd, [var])
312 Term`^(Term.inst s acc) (^fupd ^f ^var) = ^acc ^var`
317 val f = gen_var_domty("f", fupd, [var])
319 Term`^(Term.inst s acc) (^fupd ^f ^var) = ^f (^acc ^var)`
322 val tactic = STRUCT_CASES_TAC (SPEC var cases_thm) THEN
374 val f = variant [var] (mk_var("f", fty))
375 val g = variant [var,
[all...]

Completed in 182 milliseconds

1234567891011>>