@[reducible, inline]

abbrev Lake.Ellipsis : Type

Equations

• Lake.Ellipsis = Lean.TSyntax `Lean.Parser.Term.ellipsis

@[reducible, inline]

abbrev Lake.NamedArgument : Type

@[reducible, inline]

abbrev Lake.Argument : Type

instance Lake.instCoeTermArgument : Coe Lean.Term Lake.Argument

instance Lake.instCoeEllipsisArgument : Coe Lake.Ellipsis Lake.Argument

instance Lake.instCoeNamedArgumentArgument : Coe Lake.NamedArgument Lake.Argument

@[reducible, inline]

abbrev Lake.Hole : Type

@[reducible, inline]

abbrev Lake.BinderIdent : Type

@[reducible, inline]

abbrev Lake.TypeSpec : Type

def Lake.mkHoleFrom (ref : Lean.Syntax) : Lake.Hole

instance Lake.instCoeHoleTerm : Coe Lake.Hole Lean.Term

Equations

• Lake.instCoeHoleTerm = { coe := fun (s : Lake.Hole) => { raw := s.raw } }

instance Lake.instCoeHoleBinderIdent : Coe Lake.Hole Lake.BinderIdent

instance Lake.instCoeIdentBinderIdent : Coe Lean.Ident Lake.BinderIdent

Equations

• Lake.instCoeIdentBinderIdent = { coe := fun (s : Lean.Ident) => { raw := s.raw } }

@[reducible, inline]

abbrev Lake.BracketedBinder : Type

@[reducible, inline]

abbrev Lake.FunBinder : Type

instance Lake.instCoeBinderIdentFunBinder : Coe Lake.BinderIdent Lake.FunBinder

Equations

• Lake.instCoeBinderIdentFunBinder = { coe := fun (s : Lake.BinderIdent) => { raw := s.raw } }

def Lake.binder : Lean.Parser.Parser

@[reducible, inline]

abbrev Lake.Binder : Type

instance Lake.instCoeBinderTSyntaxConsSyntaxNodeKindIdentKindMkStr4Nil : Coe Lake.Binder (Lean.TSyntax [Lean.identKind, `Lean.Parser.Term.hole, `Lean.Parser.Term.bracketedBinder])

@[reducible, inline]

abbrev Lake.BinderModifier : Type

structure Lake.BinderSyntaxView : Type

• id : Lean.Ident
• type : Lean.Term
• info : Lean.BinderInfo
• modifier? : Option Lake.BinderModifier

def Lake.expandOptType (ref optType : Lean.Syntax) : Lean.Term

Equations

• Lake.expandOptType ref optType = if optType.isNone = true then { raw := (Lake.mkHoleFrom ref).raw } else { raw := optType[0][1] }

def Lake.getBinderIds (ids : Lean.Syntax) : Lean.MacroM (Array Lake.BinderIdent)

Equations

• One or more equations did not get rendered due to their size.

def Lake.expandBinderIdent (stx : Lean.Syntax) : Lean.MacroM Lean.Ident

Equations

• One or more equations did not get rendered due to their size.

def Lake.expandOptIdent (stx : Lean.Syntax) : Lake.BinderIdent

def Lake.expandBinderType (ref stx : Lean.Syntax) : Lean.Term

def Lake.expandBinderModifier (optBinderModifier : Lean.Syntax) : Option Lake.BinderModifier

def Lake.matchBinder (stx : Lean.Syntax) : Lean.MacroM (Array Lake.BinderSyntaxView)

def Lake.BinderSyntaxView.mkBinder : Lake.BinderSyntaxView → Lean.MacroM Lake.Binder

def Lake.BinderSyntaxView.mkArgument : Lake.BinderSyntaxView → Lean.MacroM Lake.NamedArgument

def Lake.expandBinders (dbs : Array Lake.Binder) : Lean.MacroM (Array Lake.Binder × Array Lean.Term)