{motive : Lean.ParserCompiler.CombinatorAttribute → Sort u} →
  ((impl : Lean.AttributeImpl) →
      (ext : Lean.SimplePersistentEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap Lean.Name)) →
        motive { impl := impl, ext := ext }) →
    (t : Lean.ParserCompiler.CombinatorAttribute) → motive t