Lines Matching defs:lhs
124 | ftree_each (FUN_LET (lhs,rhs,t)) = let
126 in lets (xs,FUN_LET (lhs,rhs2,ftree_each t)) end
199 val aux = filter (fn (lhs,rhs) => not (mem x (free_vars rhs))) aux
213 val (lhs,rhs) = dest_eq x
218 val bases = filter (not o can (match_term lhs)) (leaves (tm2ftree rhs))
219 in (car lhs, (cdr lhs, hd bases)) end
249 | ftree_each (FUN_LET (lhs,rhs,t)) = let
252 val rs2 = parallel_assign lhs y
254 handle HOL_ERR _ => FUN_LET (lhs,rhs,ftree_each t)
273 | vars (FUN_LET (lhs,rhs,t)) = all_distinct (free_vars lhs @ free_vars rhs @ vars t)
306 | live (FUN_LET (lhs,rhs,t)) = let
308 val vs = (filter ok_var (free_vars lhs))
312 val t = if ii = [] then add_live_set ls (FUN_LET (lhs,rhs,tt)) else
313 add_live_set ls (add_live_set2 ls2 ii (FUN_LET (lhs,rhs,tt)))
317 | collect (FUN_LET (lhs,rhs,t)) = collect t
452 | is_rec (FUN_LET (lhs,rhs,t)) = is_rec t
460 | count v (FUN_LET (lhs,rhs,t2)) s = let
464 in count v t2 (occ v lhs (occ v rhs (inner_s + s))) end