TRY_CONV : conv -> conv

SYNOPSIS

Attempts to apply a conversion; applies identity conversion in case of failure.

DESCRIPTION

TRY_CONV c `t` attempts to apply the conversion c to the term `t`; if this fails, then the identity conversion is applied instead giving the reflexive theorem |- t = t.

FAILURE CONDITIONS

Never fails.

EXAMPLE

  # num_CONV `0`;;
  Exception: Failure "num_CONV".
  # TRY_CONV num_CONV `0`;;
  val it : thm = |- 0 = 0

SEE ALSO

ALL_CONV.