structure Lean.ParserCompiler.CombinatorAttribute : Type

• impl : Lean.AttributeImpl
• ext : Lean.SimplePersistentEnvExtension (Lake.Name × Lake.Name) (Lake.NameMap Lake.Name)

Instances For

• Lean.ParserCompiler.instInhabitedCombinatorAttribute

instance Lean.ParserCompiler.instInhabitedCombinatorAttribute : Inhabited Lean.ParserCompiler.CombinatorAttribute

Equations

• Lean.ParserCompiler.instInhabitedCombinatorAttribute = { default := { impl := default, ext := default } }

def Lean.ParserCompiler.registerCombinatorAttribute (name : Lake.Name) (descr : String) (ref : autoParam Lake.Name _auto✝) : IO Lean.ParserCompiler.CombinatorAttribute

Equations

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

def Lean.ParserCompiler.CombinatorAttribute.getDeclFor? (attr : Lean.ParserCompiler.CombinatorAttribute) (env : Lean.Environment) (parserDecl : Lake.Name) : Option Lake.Name

Equations

• attr.getDeclFor? env parserDecl = (attr.ext.getState env).find? parserDecl

def Lean.ParserCompiler.CombinatorAttribute.setDeclFor (attr : Lean.ParserCompiler.CombinatorAttribute) (env : Lean.Environment) (parserDecl : Lake.Name) (decl : Lake.Name) : Lean.Environment

Equations

• attr.setDeclFor env parserDecl decl = Lean.PersistentEnvExtension.addEntry attr.ext env (parserDecl, decl)

unsafe def Lean.ParserCompiler.CombinatorAttribute.runDeclFor {α : Type} (attr : Lean.ParserCompiler.CombinatorAttribute) (parserDecl : Lake.Name) : Lean.CoreM α