Searched refs:zero (Results 126 - 150 of 328) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_logicScript.sml255 val zero = ``mConst (Val 0)`` value
348 (^pequal (^add [^a;^b]) (^add [^zero;^b])));
349 (* Axiom 31. plus-of-zero-when-natural *)
351 (^pequal (^add [^a;^zero]) ^a));
357 (* Axiom 34. less-of-zero-right *)
358 (^pequal (^less [^a;^zero]) ^nnil);
359 (* Axiom 35. less-of-zero-left-when-natp *)
361 (^pequal (^less [^zero;^a]) (^iff [^eequal [^a;^zero];^nnil;^t])));
364 (^pequal (^less [^a;^b]) (^less [^zero;
[all...]
/seL4-l4v-10.1.1/HOL4/examples/computability/turingMachines/
H A Dregister_machineScript.sml145 Clear (r) = set r to zero
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/
H A Dproof4.ml189 % Case: run, button = F, zero, opcode is 2 (JZR) ====================== %
H A Dproof6.ml37 % 'abs_zero' is a constant defining the zero case predicate in the %
47 % 'abs_non_zero' is a constant defining the non-zero case predicate %
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/
H A DPainting.sml119 (* If the update area is empty the result is zero. *)
H A DBitmap.sml294 argument and setting bitsPerPixel to zero in the BITMAPINFO argument
295 simply fills in the BITMAPINFOHEADER. With bitsPerPixel non-zero it
/seL4-l4v-10.1.1/HOL4/src/rational/
H A DratSyntax.sml186 val (n, f) = if Arbint.<(i,Arbint.zero) then (Arbint.~ i, mk_rat_ainv)
/seL4-l4v-10.1.1/HOL4/src/real/
H A DrealSyntax.sml80 if Arbint.<(i,Arbint.zero) then mk_negated(posint(Arbint.~ i))
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/
H A Dres_quanLib.sig17 main/zero/1.0/legalcode>. This should not be interpreted as a personal
/seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/
H A Dx64_compilerLib.sml17 val counter = ref (Arbnum.zero)
/seL4-l4v-10.1.1/HOL4/Manual/Quick/
H A Dquick.tex182 \hol{Drule}{SPECL} [\var{terms}] & specializes zero or more variables in the conclusion of a theorem \\
186 \hol{Drule}{ISPECL} [\var{terms}] & specializes theorem zero or more times, with type instantiation if necessary \\
189 \hol{Drule}{GENL} [\var{terms}] & generalizes zero or more variables in the conclusion of a theorem \\
210 \hol{numLib}{num_CONV} & equates a non-zero numeral with the form $\mathrm{SUC}\ x$ for some $x$ \\
/seL4-l4v-10.1.1/isabelle/src/Pure/General/
H A Djson.scala108 (zero | positive) ~ opt(number_fract) ~ opt(number_exp) ^^
117 def zero = one(character(c => c == '0'))
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DBoolArray.sml77 (* Make a array initialised to zero. *)
170 zero. *)
184 (* TODO: If dest_bit is zero we can simply move the bytes. If len
417 (* Copy one array into another. The arrays could be the same but in that case di must be zero. *)
H A DThread.sml267 Word 4: Maximum ML stack size. Unlimited is stored here as zero
314 will be non-zero. *)
335 if n <= 0 then raise Thread "The stack size must be greater than zero" else n
443 by zero but if it was already locked it will be some negative value. When it
446 zero or negative. In that case the unlocking thread needs to call in to the
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Djson.scala108 (zero | positive) ~ opt(number_fract) ~ opt(number_exp) ^^
117 def zero = one(character(c => c == '0'))
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A DFeedback.sml185 then raise ERR "register_trace" "Can't have trace values less than zero."
231 "Can't have trace values less than zero."
/seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/
H A Dsummary.tex187 Generalizes zero or more variables to restricted universal quantification
209 Specializes zero or more variables in the conclusion of a restricted
/seL4-l4v-10.1.1/HOL4/src/n-bit/
H A DblastLib.sml300 mk_sums Arbnum.zero
357 mk_c Arbnum.zero (BCARRY_def |> Thm.CONJUNCT1 |> Drule.SPECL [x,y,c])
555 handle HOL_ERR _ => (Arbnum.zero, Arbnum.zero)
557 if sz = Arbnum.zero orelse Arbnum.< (n, Arbnum.fromInt 11)
1089 bit_theorem Arbnum.zero []
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/
H A Dbvec.c209 vector will have the LSB at position zero. *}
289 DESCR {* Returns non-zero if the vector {\tt v} consists of only constant
290 true or false BDDs. Otherwise zero is returned. This test should
313 or false BDDs. The LSB is assumed to be at position zero. *}
752 bvec zero = bvec_build(divisor.bitnum, bddfalse); local
756 sub.bitvec[n] = bdd_ite(isSmaller, divisor.bitvec[n], zero.bitvec[n]);
766 bvec_free(zero);
/seL4-l4v-10.1.1/seL4/manual/parts/
H A Dthreads.tex169 a label of zero, the thread will be restarted. Additionally, if the
170 message length is non-zero, the faulting thread's register set will be
179 divide a number by zero.
183 a label of zero, the thread will be restarted. Additionally, if the
184 message length is non-zero, the faulting thread's register set will be
297 should be set to \texttt{1} when single-stepping, or any non-zero integer value to skip that many
/seL4-l4v-10.1.1/HOL4/src/patricia/
H A DpatriciaLib.sml45 fun even n = Arbnum.mod2 n = Arbnum.zero
50 if x = 0 orelse n = Arbnum.zero
51 then Arbnum.zero
64 fun lt_2exp x n = x = Arbnum.zero orelse Arbnum.toInt (Arbnum.log2 x) < n
182 fun l2n [] = Arbnum.zero
/seL4-l4v-10.1.1/HOL4/src/datatype/
H A DEnumType.sml56 (* thm of form x < n, where n is a non-zero numeral *)
73 (* nlt_thm is of the form |- n < x where x is non-zero *)
132 Make a size definition for an enumerated type (everywhere zero)
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DNorm_arith.sml165 in if (aval = zero) then SPEC b ZERO_MULT
167 else if (bval = zero) then SPEC a MULT_ZERO
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/
H A Dcombin.tex167 il secondo pu� essere raggiunto dal primo in zero o pi� passi. Questa
177 con zero o pi� ``passi'' della relazione $R$. (La notazione
180 che � sempre possibile andare da $x$ a $x$ in zero o pi�
184 zero o pi� passi per andare da $y$ a $z$, allora � possibile fare
185 zero o pi� passi per andare da $x$ a $z$. La realizzazione di
318 Cos�, da $y$ possiamo fare zero o pi� passi per arrivare a $u$ e
494 un passo verso $z$, e abbiamo bisogno di trovare un qualche posto raggiungibile in zero o
671 $y$ sia $v$ si possono connettere in zero o pi� passi, ma al fine di
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/
H A Djedit_editor.scala251 (Line.Position.zero /:

Completed in 151 milliseconds

1234567891011>>