Documentation
Lake
.
DSL
.
DeclUtil
Search
Google site search
Lake
.
DSL
.
DeclUtil
source
Imports
Init
Lake.Util.Binder
Lean.Parser.Command
Imported by
Lake
.
DSL
.
DocComment
Lake
.
DSL
.
Attributes
Lake
.
DSL
.
AttrInstance
Lake
.
DSL
.
WhereDecls
Lake
.
DSL
.
expandAttrs
Lake
.
DSL
.
structVal
Lake
.
DSL
.
declValDo
Lake
.
DSL
.
declValStruct
Lake
.
DSL
.
declValTyped
Lake
.
DSL
.
declValOptTyped
Lake
.
DSL
.
simpleDeclSig
Lake
.
DSL
.
structDeclSig
Lake
.
DSL
.
bracketedSimpleBinder
Lake
.
DSL
.
simpleBinder
Lake
.
DSL
.
SimpleBinder
Lake
.
DSL
.
expandOptSimpleBinder
Lake
.
DSL
.
fixName
Lake
.
DSL
.
mkConfigStructDecl
source
@[inline, reducible]
abbrev
Lake
.
DSL
.
DocComment
:
Type
Instances For
source
@[inline, reducible]
abbrev
Lake
.
DSL
.
Attributes
:
Type
Instances For
source
@[inline, reducible]
abbrev
Lake
.
DSL
.
AttrInstance
:
Type
Instances For
source
@[inline, reducible]
abbrev
Lake
.
DSL
.
WhereDecls
:
Type
Instances For
source
def
Lake
.
DSL
.
expandAttrs
(attrs? :
Option
Lake.DSL.Attributes
)
:
Array
Lake.DSL.AttrInstance
Instances For
source
def
Lake
.
DSL
.
structVal
:
Lean.ParserDescr
Instances For
source
def
Lake
.
DSL
.
declValDo
:
Lean.ParserDescr
Instances For
source
def
Lake
.
DSL
.
declValStruct
:
Lean.ParserDescr
Instances For
source
def
Lake
.
DSL
.
declValTyped
:
Lean.ParserDescr
Instances For
source
def
Lake
.
DSL
.
declValOptTyped
:
Lean.ParserDescr
Instances For
source
def
Lake
.
DSL
.
simpleDeclSig
:
Lean.ParserDescr
Instances For
source
def
Lake
.
DSL
.
structDeclSig
:
Lean.ParserDescr
Instances For
source
def
Lake
.
DSL
.
bracketedSimpleBinder
:
Lean.ParserDescr
Instances For
source
def
Lake
.
DSL
.
simpleBinder
:
Lean.ParserDescr
Instances For
source
@[inline, reducible]
abbrev
Lake
.
DSL
.
SimpleBinder
:
Type
Instances For
source
def
Lake
.
DSL
.
expandOptSimpleBinder
(stx? :
Option
Lake.DSL.SimpleBinder
)
:
Lean.MacroM
Lake.FunBinder
Instances For
source
def
Lake
.
DSL
.
fixName
(id :
Lean.Ident
)
:
Option
Lake.Name
→
Lean.Ident
Instances For
source
def
Lake
.
DSL
.
mkConfigStructDecl
(name? :
Option
Lake.Name
)
(doc? :
Option
Lake.DSL.DocComment
)
(attrs :
Array
Lake.DSL.AttrInstance
)
(ty :
Lean.Term
)
(spec :
Lean.Syntax
)
:
Lean.MacroM
Lean.Command
Instances For