Lines Matching defs:ts
10 | t::ts => let
13 NONE => recurse (t::acc) ts
14 | SOME (t1, t2) => recurse acc (t2::t1::ts)
20 fun lmk mk ts = List.foldl mk (hd ts) (tl ts)
23 val ts = gstrip dest t
24 fun recurse ts = let
25 val l = length ts div 2
26 val (p,s) = split_after l ts
28 if l = 0 then hd ts
32 if length ts < 4 then ALL_CONV t
34 val btree_norm = QCONV (PURE_REWRITE_CONV [assoc]) (recurse ts)