mk_let : term * term -> term
STRUCTURE
boolSyntax
SYNOPSIS
Constructs a let term.
DESCRIPTION
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.

SEEALSO
dest_let, is_let, mk_anylet
HOL  Kananaskis-14