@[inline, reducible]

abbrev Lake.Ellipsis : Type

Equations

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

@[inline, reducible]

abbrev Lake.NamedArgument : Type

Equations

• Lake.NamedArgument = Lean.TSyntax `Lean.Parser.Term.namedArgument

@[inline, reducible]

abbrev Lake.Argument : Type

Equations

• Lake.Argument = Lean.TSyntax `Lean.Parser.Term.argument

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

Equations

• Lake.instCoeTermArgument = { coe := fun (s : Lean.Term) => { raw := s.raw } }

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

Equations

• Lake.instCoeEllipsisArgument = { coe := fun (s : Lake.Ellipsis) => { raw := s.raw } }

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

Equations

• Lake.instCoeNamedArgumentArgument = { coe := fun (s : Lake.NamedArgument) => { raw := s.raw } }

@[inline, reducible]

abbrev Lake.Hole : Type

Equations

• Lake.Hole = Lean.TSyntax `Lean.Parser.Term.hole

@[inline, reducible]

abbrev Lake.BinderIdent : Type

Equations

• Lake.BinderIdent = Lean.TSyntax `Lean.Parser.Term.binderIdent

@[inline, reducible]

abbrev Lake.TypeSpec : Type

Equations

• Lake.TypeSpec = Lean.TSyntax `Lean.Parser.Term.typeSpec

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

Equations

• Lake.mkHoleFrom ref = Lean.mkNode `Lean.Parser.Term.hole #[Lean.mkAtomFrom ref "_"]

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

Equations

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

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

Equations

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

@[inline, reducible]

abbrev Lake.BracketedBinder : Type

Equations

• Lake.BracketedBinder = Lean.TSyntax `Lean.Parser.Term.bracketedBinder

@[inline, reducible]

abbrev Lake.FunBinder : Type

Equations

• Lake.FunBinder = Lean.TSyntax `Lean.Parser.Term.funBinder

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

Equations

• Lake.binder = HOrElse.hOrElse Lean.Parser.Term.binderIdent fun (x : Unit) => Lean.Parser.Term.bracketedBinder

@[inline, reducible]

abbrev Lake.Binder : Type

Equations

• Lake.Binder = Lean.TSyntax `Lake.binder

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

Equations

• Lake.instCoeBinderTSyntaxConsSyntaxNodeKindIdentKindMkStr4Nil = { coe := fun (stx : Lake.Binder) => { raw := stx.raw } }

@[inline, reducible]

abbrev Lake.BinderModifier : Type

Equations

• Lake.BinderModifier = Lean.TSyntax [`Lean.Parser.Term.binderTactic, `Lean.Parser.Term.binderDefault]

structure Lake.BinderSyntaxView : Type

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

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

Equations

• Lake.expandOptType ref optType = if Lean.Syntax.isNone optType = 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

Equations

• Lake.expandOptIdent stx = if Lean.Syntax.isNone stx = true then { raw := (Lake.mkHoleFrom stx).raw } else { raw := stx[0] }

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

Equations

• Lake.expandBinderType ref stx = if (Lean.Syntax.getNumArgs stx == 0) = true then { raw := (Lake.mkHoleFrom ref).raw } else { raw := stx[1] }

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

Equations

• Lake.expandBinderModifier optBinderModifier = if Lean.Syntax.isNone optBinderModifier = true then none else some { raw := optBinderModifier[0] }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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