citp def

:def <symbol> = { <ctf> | <csp> | <init> }

Assigns a name to a specific case splitting (:ctf or :csp) or induction :ind), so that it can be used as tactics in :apply.

Related: citp

Example

:def name-0 = :ind { :on (<Variable>...) :base <Term> . :step <Term> . }
:def name-1 = :ctf [ <Term> . ]
:def name-2 = :ctf-{ eq LHS = RHS . }
:def name-3 = :csp { eq lhs1 = rhs1 . eq lhs2 = rhs2 . }
:def name-4 = :csp-{ eq lhs3 = rhs3 . eq lhs4 = rhs4 . }
:apply(name-0 TC name-1 name-2 name-3 name-4)