mk_pair
pairSyntax.mk_pair : term * term -> term
Constructs object-level pair from a pair of terms.
mk_pair (t1,t2) returns (t1,t2).
Failure
Never fails.
See also
pairSyntax.dest_pair,
pairSyntax.is_pair,
pairSyntax.list_mk_pair
Press ← or → to navigate between chapters
Press S or / to search in the book
Press ? to show this help
Press Esc to hide this help
mk_pairpairSyntax.mk_pair : term * term -> term
Constructs object-level pair from a pair of terms.
mk_pair (t1,t2) returns (t1,t2).
Never fails.
pairSyntax.dest_pair,
pairSyntax.is_pair,
pairSyntax.list_mk_pair