lhs : term -> term
STRUCTURE
boolSyntax
SYNOPSIS
Returns the left-hand side of an equation.
DESCRIPTION
If
M
has the form
t1 = t2
then
lhs M
returns
t1
.
FAILURE
Fails if the term is not an equation.
SEEALSO
rhs
,
dest_eq
,
mk_eq
HOL
Kananaskis-13