- impl : AttributeImpl
Instances For
def
Lean.ParserCompiler.registerCombinatorAttribute
(name : Name)
(descr : String)
(ref : Name := by exact decl_name%)
:
Equations
Instances For
def
Lean.ParserCompiler.CombinatorAttribute.getDeclFor?
(attr : CombinatorAttribute)
(env : Environment)
(parserDecl : Name)
:
Equations
Instances For
def
Lean.ParserCompiler.CombinatorAttribute.setDeclFor
(attr : CombinatorAttribute)
(env : Environment)
(parserDecl decl : Name)
:
Equations
Instances For
unsafe def
Lean.ParserCompiler.CombinatorAttribute.runDeclFor
{α : Type}
(attr : CombinatorAttribute)
(parserDecl : Name)
:
CoreM α