----------------------------------------------------------------------
strip_neg                                                 (boolSyntax)
----------------------------------------------------------------------
strip_neg : term -> term * int

SYNOPSIS
Breaks iterated negations down to an unnegated core.

DESCRIBE
If {M} is of the form {~...~t}, then {strip_neg M} returns {(t,n)}, where
{n} is the number of consecutive negations being applied to {t}.

FAILURE
Never fails.

EXAMPLE

- strip_neg (Term `~~~~t`);
> val it = (`t`, 4) : term * int

- strip_neg (Term `x`);
<<HOL message: inventing new type variable names: 'a>>
> val it = (`x`, 0) : term * int




COMMENTS
There is no corresponding entrypoint for building iterated negations.
If such functionality is desired, {funpow} may be used:

    - funpow 3 mk_neg T;
    > val it = `~~~T` : term




SEEALSO
boolSyntax.dest_neg, boolSyntax.mk_neg, Lib.funpow.

----------------------------------------------------------------------