dest_forall

boolSyntax.dest_forall : term -> term * term

Breaks apart a universally quantified term into quantified variable and body.

If M has the form !x. t, then dest_forall M returns (x,t).

Failure

Fails if M is not a universal quantification.

See also

boolSyntax.mk_forall, boolSyntax.is_forall, boolSyntax.strip_forall, boolSyntax.list_mk_forall