strip_imp
boolSyntax.strip_imp : term -> term list * term
Iteratively breaks apart implications.
If M is of the form t1 ==> (... (tn ==> t) ...), then strip_imp M
returns ([t1,...,tn],t). Note that
strip_imp(list_mk_imp([t1,...,tn],t))
will not return ([t1,...,tn],t) if t is an implication.
Failure
Never fails.
Example
> strip_imp "(T ==> F) ==> (T ==> F)";;
Exception- Type error in function application.
Function: strip_imp : term -> term list * term
Argument: "(T ==> F) ==> (T ==> F)" : string
Reason:
Can't unify term (*Created from opaque signature*) with
string (*In Basis*) (Different type constructors)
Fail "Static Errors" raised
> strip_imp (Term `t1 ==> t2 ==> t3 ==> ~t`);
val it = ([“t1”, “t2”, “t3”, “t”], “F”): term list * term