Documentation

Lean.ParserCompiler.Attribute

structure Lean.ParserCompiler.CombinatorAttribute:

Type

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

instance Lean.ParserCompiler.instInhabitedCombinatorAttribute:

Inhabited Lean.ParserCompiler.CombinatorAttribute

Equations

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

def Lean.ParserCompiler.registerCombinatorAttribute (name : Lean.Name) (descr : String) :

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 : Lean.Name) :

Option Lean.Name

Equations

Lean.ParserCompiler.CombinatorAttribute.getDeclFor? attr env parserDecl = Lean.NameMap.find? (Lean.SimplePersistentEnvExtension.getState attr.ext env) parserDecl

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

Lean.Environment

Equations

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

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

Equations

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