is_let : term -> bool
STRUCTURE
SYNOPSIS
Tests a term to see if it is a let-expression.
DESCRIPTION
If tm is a term of the form LET M N, then dest_let tm returns true. Otherwise, it returns false.
FAILURE
Never fails.
EXAMPLE
- Term `LET f x`;
<<HOL message: inventing new type variable names: 'a, 'b>>
> val it = `LET f x` : term

- is_let it;
> val it = true : bool

- is_let (Term `let x = P /\ Q in x \/ x`);
> val it = true : bool

SEEALSO
HOL  Kananaskis-13