(motive : Lean.ParserDescr → Sort u_1) →
  (x : Lean.ParserDescr) →
    ((n : Lean.Name) → motive (Lean.ParserDescr.const n)) →
      ((n : Lean.Name) → (d : Lean.ParserDescr) → motive (Lean.ParserDescr.unary n d)) →
        ((n : Lean.Name) → (d₁ d₂ : Lean.ParserDescr) → motive (Lean.ParserDescr.binary n d₁ d₂)) →
          ((k : Lean.SyntaxNodeKind) → (prec : ℕ) → (d : Lean.ParserDescr) → motive (Lean.ParserDescr.node k prec d)) →
            ((n : String) →
                (k : Lean.SyntaxNodeKind) → (d : Lean.ParserDescr) → motive (Lean.ParserDescr.nodeWithAntiquot n k d)) →
              ((p : Lean.ParserDescr) →
                  (sep : String) → (psep : Lean.ParserDescr) → (trail : Bool) → motive (p.sepBy sep psep trail)) →
                ((p : Lean.ParserDescr) →
                    (sep : String) → (psep : Lean.ParserDescr) → (trail : Bool) → motive (p.sepBy1 sep psep trail)) →
                  ((k : Lean.SyntaxNodeKind) →
                      (prec lhsPrec : ℕ) →
                        (d : Lean.ParserDescr) → motive (Lean.ParserDescr.trailingNode k prec lhsPrec d)) →
                    ((tk : String) → motive (Lean.ParserDescr.symbol tk)) →
                      ((tk : String) →
                          (includeIdent : Bool) → motive (Lean.ParserDescr.nonReservedSymbol tk includeIdent)) →
                        ((tk asciiTk : String) →
                            (preserve : Bool) → motive (Lean.ParserDescr.unicodeSymbol tk asciiTk preserve)) →
                          ((constName : Lean.Name) → motive (Lean.ParserDescr.parser constName)) →
                            ((catName : Lean.Name) → (prec : ℕ) → motive (Lean.ParserDescr.cat catName prec)) → motive x