Lean4
/-- `mk_iff_of_inductive_prop i r` makes an `iff` rule for the inductively-defined proposition `i`.
The new rule `r` has the shape `∀ ps is, i as ↔ ⋁_j, ∃ cs, is = cs`, where
* `ps` are the type parameters,
* `is` are the indices,
* `j` ranges over all possible constructors,
* the `cs` are the parameters for each of the constructors, and
* the equalities `is = cs` are the instantiations for
each constructor for each of the indices to the inductive type `i`.
In each case, we remove constructor parameters (i.e. `cs`) when the corresponding equality would
be just `c = i` for some index `i`.
For example, `mk_iff_of_inductive_prop` on `List.Chain` produces:
```lean
∀ { α : Type*} (R : α → α → Prop) (a : α) (l : List α),
Chain R a l ↔ l = [] ∨ ∃ (b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
```
See also the `mk_iff` user attribute.
-/
@[command_parser 1000]
public meta def mkIffOfInductiveProp : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.MkIff.mkIffOfInductiveProp 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "mk_iff_of_inductive_prop ") (ParserDescr.const✝ `ident))
(ParserDescr.const✝ `ppSpace))
(ParserDescr.const✝ `ident))
