/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | LargeWord.sml | 116 NONE => (* No valid number after it, return the zero .*) 244 val zero: largeword = shortToWord 0 value 255 fun topBitClear (x: largeword) : bool = (x andb topBitAsLargeWord) = zero 275 val zero = zero value 279 fun ~ x = zero - x
|
H A D | NetServDB.sml | 35 (* The RTS calls return either zero or the address of the entry. *)
|
/seL4-l4v-10.1.1/HOL4/src/datatype/record/ |
H A D | RecordType.sml | 47 fun foldr f zero [] = zero 48 | foldr f zero (x::xs) = f x (foldr f zero xs) 49 fun foldl f zero [] = zero 50 | foldl f zero (x::xs) = foldl f (f zero x) xs
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | NumRelNorms.sml | 125 val zero = Arbint.zero value
|
H A D | Solve.sml | 56 filter (fn (const,bind) => (null bind) andalso (const < zero)) coeffsl 61 (map (fn v => (zero, [(v,one)])) var_names) @ coeffsl
|
H A D | Gen_arith.sml | 33 (* evaluates to zero. This is used because, when normalised, zero multiplied *) 34 (* by an expression is zero and hence any variables in the expression can be *)
|
/seL4-l4v-10.1.1/HOL4/src/num/reduce/Manual/ |
H A D | description.tex | 58 \item If the first numeral is zero, we need only specialize the first 65 \item If the first numeral is not zero, then we call the conversion
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | codegen_armLib.sml | 21 if i = Arbnum.zero then ["mov? " ^ r d ^ ", #0"] else let 128 (* zero *) if tm = ``aS1 psrZ`` then ("eq","ne") else
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
H A D | BUILTINS.sml | 45 | ShiftRightLogical (* Logical shift - zero added bits. *) 56 | AtomicReset (* Set a value to (tagged) zero atomically. *)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Admin/ |
H A D | ci_profile.scala | 60 (Timing.zero /: timings)(_ + _)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/ |
H A D | ci_profile.scala | 60 (Timing.zero /: timings)(_ + _)
|
/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | Subst.sml | 39 * - shifts and lifts always collapsed (and non-zero)
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | wordsSyntax.sml | 429 if n = Arbnum.zero orelse m = Arbnum.zero 430 then Arbnum.zero 434 if Arbnum.mod2 m = Arbnum.zero then v else Arbnum.plus1 v
|
H A D | fcpSyntax.sml | 24 if mod2 n = zero then 25 if n = zero then 26 raise ERR "mk_numeric_type" "must be non-zero"
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | ppc_encodeLib.sml | 36 in if Arbint.<=(Arbint.zero,i) then fill n (Arbnum.toBinString(Arbint.toNat i))
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
H A D | Algebra.sml | 163 val zero = Sum explEmpty; value 167 fun fromInt 0 = zero 329 if Map.null ms then zero
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/lib/ |
H A D | BitsN.sml | 21 fun zero s = B (0, s) function 40 fun fromBool s = fn true => one s | false => zero s 126 then Bitstring.zero b @ l
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_encodeLib.sml | 43 fun extract_int ("-",(1,x)) = Arbint.-(Arbint.zero,Arbint.fromString x) 46 fun sum [] = Arbint.zero | sum (i::is) = Arbint.+(i,sum is) 73 if Arbint.<=(Arbint.zero,i) then fill n (Arbnum.toHexString(Arbint.toNat i))
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
H A D | numerics.tex | 8 zero and successor, so it works well with inductive proofs and primitive 47 The constants \cdx{0} and \cdx{1} are overloaded. They denote zero and one, 126 small literals by zero and successor: 170 \index{division!by zero}% 172 zero yields zero: 201 There are no negative natural numbers, so \isa{m\ -\ n} equals zero unless 295 \isa{c} to be positive. Since division by zero yields zero, we could allow 296 \isa{c} to be zero [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | numerics.tex | 8 zero and successor, so it works well with inductive proofs and primitive 47 The constants \cdx{0} and \cdx{1} are overloaded. They denote zero and one, 126 small literals by zero and successor: 170 \index{division!by zero}% 172 zero yields zero: 201 There are no negative natural numbers, so \isa{m\ -\ n} equals zero unless 295 \isa{c} to be positive. Since division by zero yields zero, we could allow 296 \isa{c} to be zero [all...] |
/seL4-l4v-10.1.1/HOL4/src/floating-point/ |
H A D | binary_ieeeLib.sml | 3 The evaluation of rounding (to zero and nearest) uses a certification 63 fun is_negative_rat r = Arbrat.< (r, Arbrat.zero) 65 fun lg2 n = if n = Arbnum.zero then Arbnum.zero else Arbnum.log2 n 72 fun evenfloat (s: bool, e: Arbnum.num, f) = Arbnum.mod2 f = Arbnum.zero 91 if e = Arbnum.zero 102 if e = Arbnum.zero andalso f = Arbnum.zero 107 then (s, Arbnum.plus1 e, Arbnum.zero) 122 if e = Arbnum.zero [all...] |
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | CooperShell.sml | 384 if c1 = c2 then (zero,zero) 387 if Arbint.<(c1, c2) then (one,zero) else (zero,one) 389 if Arbint.<(c1, c2) then (zero,one) else (one,zero) 408 handle Binarymap.NotFound => (zero,zero) 424 handle Binarymap.NotFound => Arbint.zero) 427 handle Binarymap.NotFound => Arbint.zero [all...] |
H A D | OmegaSymbolic.sml | 87 val cf = if is_neg t orelse is_divides t then Arbint.zero 90 if cf = Arbint.zero then 93 else if Arbint.<(cf, Arbint.zero) then 489 { maxupc = ref Arbint.zero, maxloc = ref Arbint.zero, 505 if Arbint.<(c_i, Arbint.zero) then (* upper bound *)
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibModel.sml | 115 val zero = f 0 and one = f 1 and two = f 2 value 116 fun func ("0",[]) = SOME zero 126 | func ("mod",[m,n]) = SOME (if n = zero then m else m mod n) 132 | pred ("is_0",[n]) = SOME (n = zero) 146 val zero = f 0 and one = f 1 and two = f 2 value 147 fun func ("0",[]) = SOME zero 161 | pred ("is_0",[m]) = SOME (m = zero)
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/ |
H A D | proof2.ml | 15 % whether the accumulator is zero or non-zero. Finally, there is % 281 % Case: mpc = 5, button = F, zero, opcode is 2 (JZR) ================== %
|