/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibOmegaint.sml | 21 in if r == zero then j else gcd' j r 25 if i < zero orelse j < zero then ERR "gcd""negative arguments to gcd" 26 else if i == zero then j else if j == zero then i
|
H A D | mlibSubsume.sml | 108 {zero : (subst * 'a) stream, 113 {zero = S.NIL, 117 fun size (SUBSUME {zero, one, many = (_,_,_,m)}) = 118 S.length zero + N.size one + M.numItems m; 120 fun add (lits |-> a) (SUBSUME {zero,one,many}) = 123 [] => {zero = S.CONS ((|<>|, a), K zero), one = one, many = many} 124 | [h] => {zero = zero, one = N.insert (h |-> (h,a)) one, many = many} 135 {zero 142 val zero = S.filter (pred o snd) zero value [all...] |
H A D | mlibArbint.sml | 17 val AZ = mlibArbnum.zero 19 val zero = (true, mlibArbnum.zero) value 46 in if r <> mlibArbnum.zero then 51 in if r <> mlibArbnum.zero then 60 if m = AZ then zero else (false, n2 -- m) 64 if m = AZ then zero else (true, n2 -- m)
|
/seL4-l4v-10.1.1/HOL4/tools-poly/poly/redirects/ |
H A D | mlibOmegaint.sml | 9 val zero = I.fromInt 0; value 47 in if r == zero then j else gcd' j r 51 if i < zero orelse j < zero then ERR "gcd""negative arguments to gcd" 52 else if i == zero then j else if j == zero then i
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | Rationals.sml | 55 (if (i = zero) then rat (zero, one) 59 in if (j' < zero) 70 if (i < zero) then rat ((~j),(~i)) 71 else if (i > zero) then rat (j,i) 79 in if (i = zero) then rat (zero,one) else rat (i,j) 87 in if (i = zero) then rat (zero,one) else rat (i,j) 91 if ((i1 = zero) orels [all...] |
H A D | GenRelNorm.sml | 21 val zero : t value 42 NONE => Binarymap.insert(bmap,t0, if left then (c,c,zero) 43 else (~c,zero,c)) 60 else if i = zero then acc 63 if l = zero then (common, ls, cons_mkf'(r,k) rs) 64 else if r = zero then (common, cons_mkf'(l,k) ls, rs) 65 else if tot < zero then (cons_mkf'(l,k) common, ls, cons_mkf'(r-l,k) rs) 101 < = Arbint.<, zero = Arbint.zero, one = Arbint.one} 130 < = Arbint.<, zero [all...] |
H A D | Term_coeffs.sml | 40 fun negate_coeffs x = ((fn n => zero - n) ## 41 (map (I ## (fn n => zero - n)))) x; 50 (* zero, the variable concerned is not entered in the new binding. *) 60 then if ((coeff1 + coeff2) = zero) 80 let fun f n = if (n < zero) then (zero - n) else zero 81 fun g (s,n) = if (n < zero) then (s,(zero - n)) 93 let fun f n = if (n > zero) the [all...] |
H A D | Int_extra.sml | 30 in if (r = zero) 34 in (if ((i < zero) orelse (j < zero))
|
H A D | Sup_Inf.sml | 75 in if (i < zero) 115 (if ((Numerator r) < zero) 119 (if ((Numerator r) < zero) 122 | SIMP_mult r Pos_inf = if ((Numerator r) < zero) then Neg_inf else Pos_inf 123 | SIMP_mult r Neg_inf = if ((Numerator r) < zero) then Pos_inf else Neg_inf; 138 in if ((Numerator coeff) = zero) 196 in if (Numerator b' < zero) then Pos_inf 197 else if (Numerator b' > zero) then 201 else if (Numerator const < zero) then Neg_inf 220 in if (Numerator b' < zero) the [all...] |
H A D | Sol_ranges.sml | 97 (if (rat_less r rat_zero) then failwith "fail" else zero) 98 | (Neg_inf,Pos_inf) => zero 103 val i1' = if (i1 < zero) then zero else i1 107 (if (rat_less r rat_zero) then zero else upper_int_of_rat r) 132 (remove (fn (name,_) => name = v) bind handle _ => ((v,zero),bind)) 158 val falses = filter (fn (n,_) => n < zero) no_vars
|
H A D | Norm_ineqs.sml | 55 (* conversion avoids adding a zero constant but does not concern itself with *) 56 (* eliminating zero terms in any other way. *) 70 (if (const = zero) 87 (* unless the whole of one side is zero. *) 128 then (const1, zero, const2 - const1) 129 else (const2, const1 - const2, zero)
|
H A D | Solve_ineqs.sml | 78 (* Multiplies both sides of a normalized inequality by a non-zero constant. *) 91 if (n = zero) then failwith "fail" 118 (* Optimized for when one or both of the arguments is zero. *) 156 and coeff2 = zero - (assoc name (snd coeffs2)) 174 (if (adds1 = (zero,[])) 185 (if (adds2 = (zero,[])) 195 if (adds1 = (zero,[])) 201 if (adds2 = (zero,[])) 227 in if (coeff < zero) then ((name, one)::occsl,occsr) 228 else if (coeff > zero) the [all...] |
/seL4-l4v-10.1.1/HOL4/src/q/ |
H A D | selftest.sml | 38 val _ = new_constant ("zero", ``:num``) 65 val glmrt3 = ([] : term list, ``f zero zero = (z:'a)``) 74 val expected_mat1a1 = ``Abbrev (b = zero)`` 109 ``!x. x * SUC (SUC zero) < y * (z + SUC zero) * (y + a)``) 111 ``!x. x * SUC (SUC zero) < y * (z + SUC zero) * (y + c)`` 119 ``!x. x * SUC (SUC zero) < y * (z + SUC zero) * ( [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | timing.scala | 15 val zero: Timing = Timing(Time.zero, Time.zero, Time.zero)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | timing.scala | 15 val zero: Timing = Timing(Time.zero, Time.zero, Time.zero)
|
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
H A D | posrealTools.sig | 12 (* Case splitting posreals into zero, finite non-zero and infinite *)
|
/seL4-l4v-10.1.1/HOL4/src/pfl/examples/ |
H A D | zero.sml | 2 (* Constant zero function. *) 55 (* Define zero *) 91 (* Recursion equations for zero *) 111 (* Equational characterization of zero. *) 243 (* Efficient executable version of zero *) 266 `zero n = if dom n then zero_0 n else exec BIG n`; 269 (* Theorem showing that exec BIG = zero in the domain of the function. *) 273 (`zero n = exec BIG n`, 277 (`dom n <=> if n=0 then T else dom (n-1) /\ dom (zero(n-1))`, 282 (zero [all...] |
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | Arbrat.sml | 24 val zero = fromInt 0 value 52 if n = Arbint.zero 54 else (if Arbint.< (n, Arbint.zero) 78 else if n < zero
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/lib/ |
H A D | Bitstring.sml | 19 fun zero n = List.tabulate (Nat.toNativeInt n, fn _ => false) function 20 fun one n = if n < 1 then [] else zero (n - 1) @ [true] 136 fun op << (l, s) = l @ zero s 154 then zero (Nat.fromNativeInt (s - n)) @ l 163 if s = Nat.zero then [false] 207 if n = Nat.zero 208 then zero n
|
/seL4-l4v-10.1.1/HOL4/src/portableML/mosml/ |
H A D | Arbintcore.sml | 20 val AZ = Arbnumcore.zero 22 val zero = (true, Arbnumcore.zero) value 46 in if r <> Arbnumcore.zero then 51 in if r <> Arbnumcore.zero then 60 if m = AZ then zero else (false, n2 -- m) 64 if m = AZ then zero else (true, n2 -- m)
|
/seL4-l4v-10.1.1/HOL4/src/rational/ |
H A D | ratReduce.sml | 6 val zero = mk_rat_of_num (numSyntax.mk_numeral Arbnum.zero) value 36 ERROR "prove_two_nonzero_preconds" "denominators not both non-zero" 91 REWR_CONV NOT_F) (mk_neg(mk_eq(neg1,zero))) |> EQT_ELIM 132 if n_i = zero then REWR_CONV RAT_DIV_0 t 135 val _ = d_i > zero orelse
|
H A D | fracLib.sig | 15 (* positive and non-zero *)
|
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
H A D | Arbnumcore.sml | 15 val zero = 0 value 27 fun less1 x = if x = 0 then raise Fail "Can't take one off zero" else x - 1 28 fun less2 x = if x < 2 then raise Fail "Can't take one off zero" else x - 2
|
H A D | Arbintcore.sml | 10 val zero = 0 value
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | wlogLib.sig | 9 icdomain/zero/1.0/legalcode>. This should not be interpreted as a personal
|