| /seL4-l4v-master/HOL4/polyml/libpolyml/ |
| H A D | timing.h | 63 operator FILETIME() const { return t; } argument
78 operator timeval() const { return t; } argument
[all...] |
| H A D | bitmap.h | 43 bool Created() const { return m_bits != 0; } argument
53 bool TestBit(uintptr_t n) const { return (m_bits[n >> 3] & BitN(n)) != 0; } argument
|
| H A D | gctaskfarm.h | 62 bool Draining(void) const { return queuedItems == 0; } argument
64 unsigned ThreadCount(void) const { return threadCount; } argument
|
| H A D | heapsizing.h | 49 bool PerformSharingPass() const { return performSharingPass; } argument
|
| /seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/calculator/ |
| H A D | hashtbl.cxx | 61 int hashTable::lookup(const char *id, hashData &d) const argument
163 unsigned int hashTable::hashval(const char *s) const argument
|
| H A D | slist.h | 40 int size(void) const { return len; } argument
41 int empty(void) const { return len==0; } argument
162 int more(void) const { return next!=NULL; } argument
168 T &operator*(void) const { return *((T*)next->data); } argument
178 T &head(void) const { return *((T*)voidSList::head->data); } argument
179 T &tail(void) const { retur argument
180 first(void) const argument
181 empty(void) const argument
182 size(void) const argument
[all...] |
| /seL4-l4v-master/HOL4/src/num/arith/src/ |
| H A D | Sup_Inf.sml | 69 else let val (const,bind) = hd ineqs value
[all...] |
| H A D | Sol_ranges.sml | 130 else let val (const,bind) = hd coeffsl value
|
| H A D | Term_coeffs.sml | 160 in (let val (const,rest) = dest_plus tm value
|
| H A D | Solve_ineqs.sml | 334 val ((const,bind),f) = value
|
| /seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | SolverTypes.h | 57 uint hash() const { return (uint)x; } argument
98 int size () const { return size_learnt >> 1; } argument
99 bool learnt () const { return size_learnt & 1; } argument
100 Lit operator [] (int i) const { return data[i]; } argument
102 float& activity () const { retur argument
103 id() const argument
126 isLit() const argument
127 lit() const argument
128 clause() const argument
129 operator ==(GClause c) const argument
130 operator !=(GClause c) const argument
[all...] |
| H A D | Global.h | 169 operator const T* (void) const { return data; } argument
172 int size (void) const { return sz; } argument
183 const T& last (void) const { retur argument
187 operator [](int index) const argument
199 copyTo(vec<T>& copy) const argument
243 toInt(void) const argument
245 operator ==(const lbool& other) const argument
246 operator !=(const lbool& other) const argument
247 operator ~(void) const argument
[all...] |
| H A D | Solver.h | 121 bool locked (const Clause* c) const { return reason[var((*c)[0])] == c; } argument
124 int decisionLevel() const { return trail_lim.size(); } argument
160 lbool value(Var x) const { return toLbool(assigns[x]); } argument
161 lbool value(Lit p) const { retur argument
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/x64_compiler/ |
| H A D | x64_compilerLib.sml | 91 val const = (repeat car o fst o dest_eq o concl o hd o CONJUNCTS) th2 value
|
| /seL4-l4v-master/HOL4/examples/muddy/ |
| H A D | bvec.sig | 5 type const = int type
|
| H A D | bvec.sml | 10 type const = int type
|
| /seL4-l4v-master/HOL4/examples/bootstrap/ |
| H A D | source_propertiesScript.sml | 300 val (const,args) = strip_comb lhs value
|
| H A D | automation_lemmasScript.sml | 484 val const = ���Const ^name��� value
|
| /seL4-l4v-master/HOL4/src/floating-point/ |
| H A D | fp-functor.sml | 26 fun const name = Term.mk_thy_const {Ty = ty, Thy = thy, Name = pre name} function
|
| /seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
| H A D | Term.sig | 19 type const = functionName type
|
| /seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Term.sig | 19 type const = functionName type
|
| /seL4-l4v-master/HOL4/examples/dev/sw/ |
| H A D | IRSyntax.sml | 180 val const = mk_comb (Term`n2w:num->word8`, mk_numeral c) value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
| H A D | IRSyntax.sml | 180 val const = mk_comb (Term`n2w:num->word8`, mk_numeral c) value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
| H A D | IRSyntax.sml | 180 val const = mk_comb (Term`n2w:num->word8`, mk_numeral c) value
|
| /seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/ |
| H A D | bvec.h | 134 bdd operator[](int i) const { return roots.bitvec[i]; } argument
135 int bitnum(void) const { return roots.bitnum; } argument
136 int empty(void) const { return roots.bitnum==0; } argument
178 operator &(const bvec &a) const argument
179 operator ^(const bvec &a) const argument
180 operator |(const bvec &a) const argument
181 operator !(void) const argument
182 operator <<(int a) const argument
183 operator <<(const bvec &a) const argument
184 operator >>(int a) const argument
185 operator >>(const bvec &a) const argument
186 operator +(const bvec &a) const argument
187 operator -(const bvec &a) const argument
188 operator *(int a) const argument
189 operator *(const bvec a) const argument
190 operator <(const bvec &a) const argument
191 operator <=(const bvec &a) const argument
192 operator >(const bvec &a) const argument
193 operator >=(const bvec &a) const argument
194 operator ==(const bvec &a) const argument
195 operator !=(const bvec &a) const argument
[all...] |