SPLICE_CONJ_CONV

Conv.SPLICE_CONJ_CONV : conv

Partially normalize a conjunction.

Normalize to right associativity a conjunction without recursing in the right conjunct.

Failure

Fails if the user-provided term is not a conjunction.

Example

> SPLICE_CONJ_CONV ``(a1 /\ a2 /\ a3) /\ b /\ c``;
val it = ⊢ (a1 ∧ a2 ∧ a3) ∧ b ∧ c ⇔ a1 ∧ a2 ∧ a3 ∧ b ∧ c: thm

> SPLICE_CONJ_CONV ``(a1 /\ a2) /\ (b1 /\ b2) /\ c``;
val it = ⊢ (a1 ∧ a2) ∧ (b1 ∧ b2) ∧ c ⇔ a1 ∧ a2 ∧ (b1 ∧ b2) ∧ c: thm