strip_neg : term -> term * int
STRUCTURE
boolSyntax
SYNOPSIS
Breaks iterated negations down to an unnegated core.
DESCRIPTION
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
dest_neg, mk_neg, funpow
HOL  Trindemossen-1