Lean4
/-- Applying the `mk_iff` attribute to an inductively-defined proposition `mk_iff` makes an `iff` rule
`r` with 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, if we try the following:
```lean
@[mk_iff]
structure Foo (m n : Nat) : Prop where
equal : m = n
sum_eq_two : m + n = 2
```
Then `#check foo_iff` returns:
```lean
foo_iff : ∀ (m n : Nat), Foo m n ↔ m = n ∧ m + n = 2
```
You can add an optional string after `mk_iff` to change the name of the generated lemma.
For example, if we try the following:
```lean
@[mk_iff bar]
structure Foo (m n : Nat) : Prop where
equal : m = n
sum_eq_two : m + n = 2
```
Then `#check bar` returns:
```lean
bar : ∀ (m n : ℕ), Foo m n ↔ m = n ∧ m + n = 2
```
See also the user command `mk_iff_of_inductive_prop`.
-/
@[attr_parser 1000]
public meta def mkIff : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.MkIff.mkIff 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "mk_iff" false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `ident))))
