dest_disj

boolSyntax.dest_disj : term -> term * term

Term destructor for disjunctions.

If M is a term having the form t1 \/ t2, then dest_disj M returns (t1,t2).

Failure

Fails if M is not a disjunction.

See also

boolSyntax.mk_disj, boolSyntax.is_disj, boolSyntax.strip_disj, boolSyntax.list_mk_disj