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

See also

boolSyntax.mk_let, boolSyntax.dest_let