is_let
boolSyntax.is_let : term -> bool
Tests a term to see if it is a let-expression.
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`;
val it = “LET f x”: term
> is_let it;
val it = true: bool
> is_let (Term `let x = P /\ Q in x \/ x`);
Exception- HOL_ERR
(at boolpp.Term: on line 1, characters 18-27: let with non-equality) raised