@[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.instCoeBinderIdentBinder
• 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

Same as mkHole but returns TSyntax.

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

Instances For

• Lake.instCoeBracketedBinderBinder

@[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 } }

@[reducible, inline]

abbrev Lake.DeclBinder : Type

Equations

• Lake.DeclBinder = Lean.TSyntax [Lean.identKind, `Lean.Parser.Term.hole, `Lean.Parser.Term.bracketedBinder]

Instances For

• Lake.instCoeBinderDeclBinder

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.instCoeBinderDeclBinder
• Lake.instCoeBinderIdentBinder
• Lake.instCoeBracketedBinderBinder

instance Lake.instCoeBinderIdentBinder : Coe BinderIdent Binder

Equations

• Lake.instCoeBinderIdentBinder = { coe := fun (stx : Lake.BinderIdent) => { raw := stx.raw } }

instance Lake.instCoeBracketedBinderBinder : Coe BracketedBinder Binder

Equations

• Lake.instCoeBracketedBinderBinder = { coe := fun (stx : Lake.BracketedBinder) => { raw := stx.raw } }

instance Lake.instCoeBinderDeclBinder : Coe Binder DeclBinder

Equations

• Lake.instCoeBinderDeclBinder = { 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]

@[reducible, inline]

abbrev Lake.DepArrow : Type

Equations

• Lake.DepArrow = Lean.TSyntax `Lean.Parser.Term.depArrow

Instances For

• Lake.instCoeDepArrowTerm

instance Lake.instCoeDepArrowTerm : Coe DepArrow Lean.Term

Equations

• Lake.instCoeDepArrowTerm = { coe := fun (stx : Lake.DepArrow) => { raw := stx.raw } }

structure Lake.BinderSyntaxView : Type

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

Instances For

• Lake.instInhabitedBinderSyntaxView
• Lake.instReprBinderSyntaxView

instance Lake.instInhabitedBinderSyntaxView : Inhabited BinderSyntaxView

Equations

• Lake.instInhabitedBinderSyntaxView = { default := { ref := default, id := default, type := default, info := default, modifier? := default } }

instance Lake.instReprBinderSyntaxView : Repr BinderSyntaxView

Equations

• Lake.instReprBinderSyntaxView = { reprPrec := Lake.reprBinderSyntaxView✝ }

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 = Option.map (fun (x : Lean.Syntax) => { raw := x }) optBinderModifier.getOptional?

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

Equations

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

@[inline]

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

Equations

• Lake.expandBinder stx = Lake.expandBinderCore #[] stx

def Lake.expandBinders (stxs : Array Lean.Syntax) : Lean.MacroM (Array BinderSyntaxView)

Equations

• Lake.expandBinders stxs = Array.foldlM Lake.expandBinderCore #[] stxs

def Lake.BinderSyntaxView.mkBinder : BinderSyntaxView → BracketedBinder

Equations

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

def Lake.BinderSyntaxView.mkDepArrow (res : Lean.Term) (self : BinderSyntaxView) : DepArrow

Equations

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

def Lake.mkDepArrow (binders : Array BinderSyntaxView) (res : Lean.Term) : Lean.Term

Equations

• Lake.mkDepArrow binders res = Array.foldl (fun (r : Lean.Term) (v : Lake.BinderSyntaxView) => { raw := (Lake.BinderSyntaxView.mkDepArrow r v).raw }) res binders

def Lake.BinderSyntaxView.mkFunBinder : BinderSyntaxView → FunBinder

Equations

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

def Lake.BinderSyntaxView.mkArgument : BinderSyntaxView → NamedArgument

Equations

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