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