Searched defs:take (Results 1 - 25 of 27) sorted by relevance

12

/seL4-l4v-master/HOL4/polyml/modules/IntInfAsInt/
H A DList.sml24 val take = fn (l, i) => take(l, FixedInt.fromInt i) value
/seL4-l4v-master/HOL4/src/portableML/
H A Dseq.sml107 fun take n l = function
[all...]
H A Dseq.sig40 val take : int -> 'a seq -> 'a list value
/seL4-l4v-master/HOL4/polyml/basis/
H A DListSignature.sml38 val take : ('a list * int) -> 'a list value
H A DList.sml70 fun take(_, 0) = [] function
/seL4-l4v-master/HOL4/examples/elliptic/
H A DStream.sig54 val take : int -> 'a stream -> 'a stream (* raises Subscript *) value
H A DStream.sml89 fun take 0 _ = NIL function
/seL4-l4v-master/HOL4/src/metis/
H A DmlibStream.sig31 val take : int -> 'a stream -> 'a stream (* raises Subscript *) value
H A DmlibStream.sml77 fun take 0 _ = NIL function
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DStream.sig55 val take : int -> 'a stream -> 'a stream (* raises Subscript *) value
H A DStream.sml88 fun take 0 _ = Nil function
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A DbackgroundLib.sig16 val take : int -> 'a list -> 'a list value
H A DbackgroundLib.sml35 fun take n [] = [] function
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DStream.sig55 val take : int -> 'a stream -> 'a stream (* raises Subscript *) value
H A DStream.sml88 fun take 0 _ = Nil function
/seL4-l4v-master/HOL4/examples/formal-languages/lambek/
H A DExampleScript.sml41 fun take ts = MAP_EVERY Q.EXISTS_TAC ts; (* from HOL mizar mode *) function
H A DCutFreeScript.sml42 fun take ts = MAP_EVERY Q.EXISTS_TAC ts; (* from HOL mizar mode *) function
H A DLambekScript.sml42 fun take ts = MAP_EVERY Q.EXISTS_TAC ts; (* from HOL mizar mode *) function
/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/
H A DL3.sig46 val take : IntInf.int * 'a list -> 'a list value
H A DL3.sml110 fun take (n, l) = List.take (l, IntInf.toInt n) function
/seL4-l4v-master/HOL4/examples/CCS/
H A DCCSLib.sml21 fun take ts = MAP_EVERY Q.EXISTS_TAC ts; (* from HOL mizar mode *) function
H A DCCSLib.sig12 val take : Q.tmquote list -> tactic value
/seL4-l4v-master/HOL4/src/refute/
H A DCanon.sml496 fun take sofar l = function
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_symbolsScript.sml356 fun take 0 xs = [] | take n xs = hd xs :: take (n-1) xs function
/seL4-l4v-master/HOL4/src/num/termination/
H A DTotalDefn.sml32 fun take 0 L = [] function

Completed in 233 milliseconds

12