mk_let

boolSyntax.mk_let : term * term -> term

Constructs a let term.

The invocation mk_let (M,N) returns the term `LET M N`. If M is of the form \x.t then the result will be pretty-printed as let x = N in t. Since LET M N is defined to be M N, one can think of a let-expression as a suspended beta-redex (if that helps).

Failure

Fails if the types of M and N are such that LET M N is not well-typed, i.e., the type of M must be a function type, and the type of N must equal the domain of the type of M.

Example

- mk_let(Term`\x. x \/ x`, Term`Q /\ R`);
> val it = `let x = Q /\ R in x \/ x` : term

Comments

let expressions may be nested.

Pairing can also be used in the let syntax, provided pairTheory has been loaded. The library pairLib provides support for manipulating ‘paired’ lets.

See also

boolSyntax.dest_let, boolSyntax.is_let, pairSyntax.mk_anylet