Searched defs:zero (Results 1 - 25 of 45) sorted by relevance

12

/seL4-l4v-master/HOL4/tools-poly/poly/redirects/
H A DmlibOmegaint.sml9 val zero = I.fromInt 0; value
/seL4-l4v-master/HOL4/src/metis/
H A DmlibArbnum.sig8 val zero : num value
H A DmlibOmegaint.sig8 val zero : int value
H A DmlibArbint.sig10 val zero : int value
H A DmlibArbint.sml19 val zero = (true, mlibArbnum.zero) value
H A DmlibSubsume.sml142 val zero = S.filter (pred o snd) zero value
[all...]
/seL4-l4v-master/HOL4/src/portableML/poly/
H A DArbintcore.sml10 val zero = 0 value
H A DArbintcore.sig8 val zero : int value
H A DArbnumcore.sig6 val zero : num value
H A DArbnumcore.sml15 val zero = 0 value
/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/
H A DBitstring.sig32 val zero: Nat.nat -> bitstring value
H A DNat.sig26 val zero: nat value
H A DNat.sml30 val zero = 0: IntInf.int value
H A DBitstring.sml19 fun zero n = List.tabulate (Nat.toNativeInt n, fn _ => false) function
/seL4-l4v-master/HOL4/src/num/arith/src/
H A DGenRelNorm.sml21 val zero : t value
[all...]
H A DArith_cons.sml108 val zero = numSyntax.zero_tm value
/seL4-l4v-master/HOL4/src/num/theories/
H A DnumScript.sml73 val zero = mk_var("0", mk_thy_type{Tyop="num",Thy="num",Args=[]}); value
/seL4-l4v-master/HOL4/src/portableML/
H A DArbrat.sig9 val zero : rat value
H A DArbrat.sml24 val zero = fromInt 0 value
/seL4-l4v-master/HOL4/src/portableML/mosml/
H A DArbintcore.sig8 val zero : int value
H A DArbintcore.sml22 val zero = (true, Arbnumcore.zero) value
H A DArbnumcore.sig6 val zero : num value
/seL4-l4v-master/HOL4/src/HolSat/vector_def_CNF/
H A DdefCNF.sml29 val zero = numSyntax.zero_tm value
/seL4-l4v-master/HOL4/src/HolSmt/
H A DZ3_ProofParser.sml179 val zero = wordsSyntax.mk_n2w (numSyntax.zero_tm, wordsSyntax.dim_of t) value
186 val zero = wordsSyntax.mk_n2w (numSyntax.zero_tm, wordsSyntax.dim_of t) value
/seL4-l4v-master/HOL4/examples/elliptic/
H A DAlgebra.sml163 val zero = Sum explEmpty; value

Completed in 231 milliseconds

12