Documentation

Lake.Util.Binder

@[reducible, inline]

abbrev Lake.Ellipsis :

Equations

Instances For

@[reducible, inline]

abbrev Lake.NamedArgument :

Equations

Instances For

@[reducible, inline]

abbrev Lake.Argument :

Equations

Instances For

instance Lake.instCoeTermArgument :

Coe Lean.Term Argument

Equations

instance Lake.instCoeEllipsisArgument :

Coe Ellipsis Argument

Equations

instance Lake.instCoeNamedArgumentArgument :

Coe NamedArgument Argument

Equations

@[reducible, inline]

abbrev Lake.Hole :

Equations

Instances For

@[reducible, inline]

abbrev Lake.BinderIdent :

Equations

Instances For

@[reducible, inline]

abbrev Lake.TypeSpec :

Equations

Instances For

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

Same as mkHole but returns TSyntax.

Equations

Instances For

instance Lake.instCoeHoleTerm :

Coe Hole Lean.Term

Equations

instance Lake.instCoeHoleBinderIdent :

Coe Hole BinderIdent

Equations

instance Lake.instCoeIdentBinderIdent :

Coe Lean.Ident BinderIdent

Equations

@[reducible, inline]

abbrev Lake.BracketedBinder :

Equations

Instances For

@[reducible, inline]

abbrev Lake.FunBinder :

Equations

Instances For

instance Lake.instCoeBinderIdentFunBinder :

Coe BinderIdent FunBinder

Equations

@[reducible, inline]

abbrev Lake.DeclBinder :

Equations

Instances For

def Lake.binder :

Lean.Parser.Parser

Equations

Instances For

@[reducible, inline]

abbrev Lake.Binder :

Equations

Instances For

instance Lake.instCoeBinderIdentBinder :

Coe BinderIdent Binder

Equations

instance Lake.instCoeBracketedBinderBinder :

Coe BracketedBinder Binder

Equations

instance Lake.instCoeBinderDeclBinder :

Coe Binder DeclBinder

Equations

@[reducible, inline]

abbrev Lake.BinderModifier :

Equations

Instances For

@[reducible, inline]

abbrev Lake.DepArrow :

Equations

Instances For

instance Lake.instCoeDepArrowTerm :

Coe DepArrow Lean.Term

Equations

structure Lake.BinderSyntaxView :

Instances For

instance Lake.instInhabitedBinderSyntaxView :

Inhabited BinderSyntaxView

Equations

instance Lake.instReprBinderSyntaxView :

Repr BinderSyntaxView

Equations

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

Equations

Instances For

def Lake.getBinderIds (ids : Lean.Syntax) :

Lean.MacroM (Array BinderIdent)

Equations

Instances For

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

Lean.MacroM Lean.Ident

Equations

Instances For

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

Equations

Instances For

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

Equations

Instances For

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

Option BinderModifier

Equations

Instances For

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

Lean.MacroM (Array BinderSyntaxView)

Equations

Instances For

@[inline]

def Lake.expandBinder (stx : Lean.Syntax) :

Lean.MacroM (Array BinderSyntaxView)

Equations

Instances For

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

Lean.MacroM (Array BinderSyntaxView)

Equations

Instances For

def Lake.BinderSyntaxView.mkBinder :

BinderSyntaxView → BracketedBinder

Equations

Instances For

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

Equations

Instances For

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

Equations

Instances For

def Lake.BinderSyntaxView.mkFunBinder :

BinderSyntaxView → FunBinder

Equations

Instances For

def Lake.BinderSyntaxView.mkArgument :

BinderSyntaxView → NamedArgument

Equations

Instances For