pairSyntax.spine

spine_pair : term -> term list

STRUCTURE

pairSyntax

LIBRARY

pair

SYNOPSIS

Breaks a paired structure into its constituent pieces.

EXAMPLE

- spine_pair (Term `((1,2),(3,4))`);
> val it = [`(1,2)`, `3`, `4`] : term list

COMMENTS

Note that spine_pair is similar, but not identical, to strip_pair which works recursively.

FAILURE

Never fails.

SEEALSO

strip_pair

HOL Kananaskis-14