LAND_CONV : conv -> conv

SYNOPSIS

Apply a conversion to left-hand argument of binary operator.

DESCRIPTION

If c is a conversion where c `l` gives |- l = l', then LAND_CONV c `op l r` gives |- op l r = op l' r.

FAILURE CONDITIONS

Fails if the underlying conversion does or returns an inappropriate theorem (i.e. is not really a conversion).

EXAMPLE

  # LAND_CONV NUM_ADD_CONV `(2 + 2) + (2 + 2)`;;
  val it : thm = |- (2 + 2) + 2 + 2 = 4 + 2 + 2