Lines Matching defs:loop
168 let fun loop (A,_) [] = A169 | loop (A,typ) (tm::rst) =172 then loop(App(A,tm),ty2) rst175 in fn (f,L) => loop(f, type_of f) L496 fun loop n = if HOLset.member(nmset, n) then loop (n ^ "'") else n498 loop n831 fun loop s =832 if mem s L orelse P s then loop (s ^ "'")834 in mk_var(loop Name, Ty)