Searched refs:zero (Results 1 - 25 of 328) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibOmegaint.sml21 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 DmlibSubsume.sml108 {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 DmlibArbint.sml17 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 DmlibOmegaint.sml9 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 DRationals.sml55 (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 DGenRelNorm.sml21 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 DTerm_coeffs.sml40 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 DInt_extra.sml30 in if (r = zero)
34 in (if ((i < zero) orelse (j < zero))
H A DSup_Inf.sml75 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 DSol_ranges.sml97 (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 DNorm_ineqs.sml55 (* 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 DSolve_ineqs.sml78 (* 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 Dselftest.sml38 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 Dtiming.scala15 val zero: Timing = Timing(Time.zero, Time.zero, Time.zero)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Dtiming.scala15 val zero: Timing = Timing(Time.zero, Time.zero, Time.zero)
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/
H A DposrealTools.sig12 (* Case splitting posreals into zero, finite non-zero and infinite *)
/seL4-l4v-10.1.1/HOL4/src/pfl/examples/
H A Dzero.sml2 (* 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 DArbrat.sml24 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 DBitstring.sml19 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 DArbintcore.sml20 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 DratReduce.sml6 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 DfracLib.sig15 (* positive and non-zero *)
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/
H A DArbnumcore.sml15 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 DArbintcore.sml10 val zero = 0 value
/seL4-l4v-10.1.1/HOL4/src/1/
H A DwlogLib.sig9 icdomain/zero/1.0/legalcode>. This should not be interpreted as a personal

Completed in 182 milliseconds

1234567891011>>