@[reducible, inline]

abbrev Lake.Ellipsis : Type

Equations

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

Instances For

• Lake.instCoeEllipsisArgument

@[reducible, inline]

abbrev Lake.NamedArgument : Type

Equations

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

Instances For

• Lake.instCoeNamedArgumentArgument

@[reducible, inline]

abbrev Lake.Argument : Type

Equations

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

Instances For

• Lake.instCoeEllipsisArgument
• Lake.instCoeNamedArgumentArgument
• Lake.instCoeTermArgument

instance Lake.instCoeTermArgument : Coe Lean.Term Argument

Equations

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

instance Lake.instCoeEllipsisArgument : Coe Ellipsis Argument

Equations

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

instance Lake.instCoeNamedArgumentArgument : Coe NamedArgument Argument

Equations

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

@[reducible, inline]

abbrev Lake.Hole : Type

Equations

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

Instances For

• Lake.instCoeHoleBinderIdent
• Lake.instCoeHoleTerm

@[reducible, inline]

abbrev Lake.BinderIdent : Type

Equations

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

Instances For

• Lake.instCoeBinderIdentFunBinder
• Lake.instCoeHoleBinderIdent
• Lake.instCoeIdentBinderIdent

@[reducible, inline]

abbrev Lake.TypeSpec : Type

Equations

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

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

Equations

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

instance Lake.instCoeHoleTerm : Coe Hole Lean.Term

Equations

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

instance Lake.instCoeHoleBinderIdent : Coe Hole BinderIdent

Equations

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

instance Lake.instCoeIdentBinderIdent : Coe Lean.Ident BinderIdent

Equations

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

@[reducible, inline]

abbrev Lake.BracketedBinder : Type

Equations

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

@[reducible, inline]

abbrev Lake.FunBinder : Type

Equations

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

Instances For

• Lake.instCoeBinderIdentFunBinder

instance Lake.instCoeBinderIdentFunBinder : Coe BinderIdent FunBinder

Equations

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

def Lake.binder : Lean.Parser.Parser

Equations

• Lake.binder = (Lean.Parser.Term.binderIdent <|> Lean.Parser.Term.bracketedBinder)

@[reducible, inline]

abbrev Lake.Binder : Type

Equations

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

Instances For

• Lake.instCoeBinderTSyntaxConsSyntaxNodeKindIdentKindMkStr4Nil

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

Equations

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

@[reducible, inline]

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 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 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) : BinderIdent

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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