Searched refs:MIN (Results 1 - 25 of 61) sorted by relevance

123

/seL4-l4v-10.1.1/seL4/src/api/
H A Dfaults.c84 for (i = 0; i < MIN(length, n_msgRegisters); i++) {
107 for (i = 0; i < MIN(length, n_msgRegisters); i++) {
132 copyMRsFaultReply(sender, receiver, MessageID_Syscall, MIN(length, n_syscallMessage));
136 copyMRsFaultReply(sender, receiver, MessageID_Exception, MIN(length, n_exceptionMessage));
/seL4-l4v-10.1.1/HOL4/src/emit/MLton/
H A DnumML.sml3 nonfix MOD DIV DIVMOD findq LEAST WHILE MAX MIN FUNPOW FACT ODD EVEN
93 fun MIN x y = (if < x y then x else y) function
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/metag/
H A Dffi.c30 #define MIN(a,b) (((a) < (b)) ? (a) : (b)) macro
96 return ALIGN(MIN(stack - argp, 6*4), 8);
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/
H A Dkernel.h175 #define MIN(a,b) ((a) < (b) ? (a) : (b)) macro
H A Dreorder.c477 maxAllowed = MIN(best/5+best, bddmaxnodesize-bddmaxnodeincrease-2);
511 maxAllowed = MIN(best/5+best,
539 maxAllowed = MIN(best/5+best,
965 levels[n].size = MIN(levels[n].maxsize, (levels[n].nodenum*5)/4);
1377 levels[var1].size = MIN(levels[var1].maxsize, levels[var1].size/2);
1379 levels[var1].size = MIN(levels[var1].maxsize, levels[var1].size*2);
H A Dbvec.c274 int minnum = MIN(bitnum, v.bitnum);
920 int n, minnum = MIN(e.bitnum,pos);
/seL4-l4v-10.1.1/seL4/include/
H A Dutil.h19 #define MIN(a,b) (((a)<(b))?(a):(b)) macro
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Darm_coretypesScript.sml231 (x >> shift, x ' (MIN (dimindex(:'a) - 1) (shift - 1)))`;
367 val MIN_LEM = Q.prove(`!a b. MIN a (MIN a b) = MIN a b`, SRW_TAC [] [MIN_DEF]);
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/
H A Darm_coretypesScript.sml235 (x >> shift, x ' (MIN (dimindex(:'a) - 1) (shift - 1)))`;
371 val MIN_LEM = Q.prove(`!a b. MIN a (MIN a b) = MIN a b`, SRW_TAC [] [MIN_DEF]);
/seL4-l4v-10.1.1/HOL4/src/n-bit/
H A DwordsScript.sml188 (FCP i. l <= i /\ i <= MIN h ^HB /\ w ' i):'a word`
192 (FCP i. i + l <= MIN h ^HB /\ w ' (i + l)):'a word`
196 (FCP i. l <= MIN h ^HB /\ w ' (MIN (i + l) (MIN h ^HB))):'a word`
1306 (n2w (SLICE (MIN h ^HB) l n)):'a word`,
1311 (n2w (BITS (MIN h ^HB) l n)):'a word`,
1312 FIELD_WORD_TAC \\ Cases_on `i + l <= MIN h ^HB`
1328 n2w (SIGN_EXTEND (MIN (SUC h) (dimindex(:'a)) - l) (dimindex(:'a))
1329 (BITS (MIN
[all...]
H A DalignmentScript.sml149 aligned p (w: 'a word) = (bit_count_upto (MIN (dimindex(:'a)) p) w = 0)`,
/seL4-l4v-10.1.1/HOL4/examples/dev/booth/
H A DboothScript.sml132 `MIN HB 1 = 1`,
151 `(!x t. MIN x (x - 2 + 2 * (t + 1)) = x) /\
152 (!x t. MIN x (x + 2 * (t + 1)) = x)`,
197 `!t x. 2 * (t + 1) <= x + 1 ==> (MIN x (2 * t + 1) = 2 * t + 1)`,
/seL4-l4v-10.1.1/HOL4/src/num/theories/
H A DarithmeticScript.sml2920 val MIN = new_definition("MIN_DEF", ���MIN m n = if m < n then m else n���); value
2930 ���!m n. MIN m n = MIN n m���,
2931 ARW [MIN] THEN FULL_SIMP_TAC bool_ss [NOT_LESS] THEN
2940 ���!m n p. MIN m (MIN n p) = MIN (MIN m n) p���,
2941 SIMP_TAC bool_ss [MIN] THE
[all...]
H A DnumSyntax.sml34 val min_tm = prim_mk_const {Name="MIN", Thy="arithmetic"}
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/
H A DtreeScript.sml264 (MIN_LIST (t::l) = FOLDR MIN t l)`
270 (!n ns. (MIN_LIST (n::ns) = if (ns = []) then n else MIN n (MIN_LIST ns))) /\
292 ``(MIN (SUC n1) (SUC n2) = SUC (MIN n1 n2)) /\
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/
H A DupdateScript.sml58 let j = MIN n lx in
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A Dselftest.sml219 (* arithmetic operators: SUC, +, -, *, /, DIV, MOD, ABS, MIN, MAX *)
282 (``MIN (x:num) y <= x``, [thm_AUTO, thm_YO]),
283 (``MIN (x:num) y <= y``, [thm_AUTO, thm_YO]),
284 (``(z:num) < x /\ z < y ==> z < MIN x y``, [thm_AUTO, thm_YO]),
285 (``MIN (x:num) y < x``, [sat_YO, sat_Z3, sat_Z3p]),
286 (``MIN (x:num) 0 = 0``, [thm_AUTO, thm_YO]),
/seL4-l4v-10.1.1/HOL4/Manual/Logic/
H A Dsemantics.tex369 \subsection{The theory {\tt MIN}}
372 The {\it minimal theory\/}\index{MIN@\ml{MIN}}\index{minimal theory, of HOL logic@minimal theory, of \HOL{} logic} \theory{MIN} is defined by:
374 \theory{MIN} =
381 Since the theory \theory{MIN} has a signature consisting only of
385 Although the theory \theory{MIN} contains only the minimal standard
391 In the implementation, the theory \theory{MIN} is given the name
400 structure as \theory{MIN}. Its signature contains the constants in
401 \theory{MIN} an
[all...]
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Logic/
H A Dsemantics.tex369 \subsection{La teoria {\tt MIN}}
372 La {\it teoria minimale\/}\index{MIN@\ml{MIN}}\index{minimal theory, della logica HOL@minimal theory, della logica \HOL{}} \theory{MIN} � definita da:
374 \theory{MIN} =
381 Dal momento che la teoria \theory{MIN} ha una firma che consiste solo di
385 Bench� la teoria \theory{MIN} contiene solo la sintassi standard
391 Nell'implementazione, alla teoria \theory{MIN} � dato il nome
400 di tipo di \theory{MIN}. La sua firma contiene le costanti in
401 \theory{MIN}
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/correctness/
H A DmultScript.sml60 `!x t. 0 < t ==> (MIN 31 (2 * t + 29) = 31)`,
168 `!x t. 0 < t ==> (MIN x (x - 2 + 2 * t) = x)`,
387 `!h m l n. SLICE h l (BITS m 0 n) = SLICE (MIN h m) l n`,
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibUseful.sml52 val MIN = 1.0; value
60 if t > MIN then (t / Real.fromInt n, res) else several n t f a
/seL4-l4v-10.1.1/HOL4/src/list/src/
H A DindexedListsScript.sml296 ���!f l1 l2. LENGTH (MAP2i f l1 l2) = MIN (LENGTH l1) (LENGTH l2)���,
/seL4-l4v-10.1.1/HOL4/examples/elliptic/
H A DUseful.sml63 val MIN = 1.0; value
71 if t > MIN then (t / Real.fromInt n, res) else several n t f a
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DUseful.sml857 val MIN = 1.0; value
865 if t > MIN then (t / Real.fromInt n, res) else several n t f a
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DUseful.sml857 val MIN = 1.0; value
865 if t > MIN then (t / Real.fromInt n, res) else several n t f a

Completed in 156 milliseconds

123