----------------------------------------------------------------------
IFC                                                             (Conv)
----------------------------------------------------------------------
IFC : conv -> conv -> conv -> conv

SYNOPSIS
Apply a conversion and branch to next conversion.

KEYWORDS
Conversion

DESCRIBE
A call to {IFC c1 c2 c3 t} applies the conversion {c1} to {t}.
If this application succeeds (or raises {UNCHANGED}) then {c2} is applied next.
Otherwise, {c3} is applied to {t}.

FAILURE
Fails when {c1} succeeds and {c2} fails, or when {c1} fails and {c3} fails.

EXAMPLE

   > IFC (RATOR_CONV BETA_CONV) BETA_CONV NO_CONV ``(\x y. x ==> y) T F``;
   val it = |- T ==> F : thm

The first {RATOR_CONV BETA_CONV} succeeds and chains successfully with the second {BETA_CONV}.


   > IFC ALL_CONV BETA_CONV (RATOR_CONV BETA_CONV) ``(\x y. x ==> y) T F``;
   Exception - BETA_CONV: not a beta redex

Although {ALL_CONV} succeeds, it does nothing, so {BETA_CONV} is not applicable.


   > IFC NO_CONV BETA_CONV (RATOR_CONV BETA_CONV) ``(\x y. x ==> y) T F``;
   val it = |- (\y. T ==> y) F : thm

The {NO_CONV} fails, so {RATOR_CONV BETA_CONV} applies.

SEEALSO
Conv.ORELSEC, Conv.REPEATC.

----------------------------------------------------------------------