instance
Lake.instCoeBinderTSyntaxConsSyntaxNodeKindIdentKindMkStr4Nil :
Coe Lake.Binder (Lean.TSyntax [Lean.identKind, `Lean.Parser.Term.hole, `Lean.Parser.Term.bracketedBinder])
- id : Lean.Ident
- type : Lean.Term
- info : Lean.BinderInfo
- modifier? : Option Lake.BinderModifier