dest_let
boolSyntax.dest_let : term -> term * term
Breaks apart a let-expression.
If M is a term of the form LET M N, then dest_let M returns
(M,N).
Example
> dest_let (Term `let x = P /\ Q in x \/ x`);
Exception- HOL_ERR
(at boolpp.Term: on line 1, characters 20-29: let with non-equality) raised
Failure
Fails if M is not of the form LET M N.