Conv.COMB

STRUCTURE

SYNOPSIS

Applies a conversion to both immediate sub-terms of an application.

DESCRIPTION

If t is an application term of the form f x, and c is a conversion, such that c maps f to |- f = f' and x to |- x = x', then COMB_CONV c maps t to |- f x = f' x'.

If one of the two sub-calls raises the UNCHANGED exception, then the result of that call is taken to be the reflexive theorem (|- x = x if c x raises the exception, for example). If both conversions raise the UNCHANGED exception, then so too does COMB_CONV c t.

FAILURE

COMB_CONV c t fails if t is not an application term, or if c fails when applied to the rator and rand of t, or if c is not in fact a conversion (i.e., a function which maps terms t to a theorem |- t = t').

SEEALSO

ABS_CONV, COMB2_CONV, SUB_CONV