Lines Matching refs:f2
19 TAILREC f1 (f2:'a->'b) g x = f2 (WHILE g f1 x)`;64 ``!f1 (f2:'a->'b) g x. TAILREC f1 f2 g x = if g x then TAILREC f1 f2 g (f1 x) else f2 x``,79 ``(f1 = f1') /\ (f2 = (f2':'a->'b)) /\ (g = g') /\ (s = s') ==>80 (TAILREC f1 f2 g = TAILREC f1' f2' g') /\