Lines Matching defs:x0
208 (b0 ��� (env,[x0],s) ---> ([list (a:'a->v) v0],s)) ���
214 ALL_DISTINCT ([name n1] ++ free_vars x0) ���
216 (env,[If Equal [x0; Const 0] x1
217 (Let (name n1) (Op Head [x0])
218 (Let (name n2) (Op Tail [x0]) x2))],s) --->
245 (b0 ��� (env,[x0],s) ---> ([option (a:'a->v) v0],s)) ���
249 (env,[If Equal [x0; Const 0] x1
250 (Let (name n) (Op Head [x0]) x2)],s) --->
288 (b0 ��� (env,[x0],s) ---> ([pair (a:'a->v) (b:'b->v) v0],s)) ���
293 ALL_DISTINCT ([name n1; name n2] ++ free_vars x0) ���
295 (env,[Let (name n1) (Op Head [x0])
296 (Let (name n2) (Op Tail [x0]) x1)],s) --->
530 val x0 = mk_var("x0",���:exp���)
532 val asm0 = mk_basic b0 x0 (mk_comb(in_inv,v0))
565 mk_conj(b_tm,���ALL_DISTINCT (^ns ++ free_vars ^x0)���)
573 val code = if is_enum then list_mk_comb(���case_enum���,[x0,x])
574 else list_mk_comb(���case_tree���,[x0,x])