def Lean.Compiler.LCNF.mkOrderedDeclSetExt : IO (EnvExtension (List Name × NameSet))

Creates a replayable local environment extension holding a name set and the list of names in the order they were added to the set.

Equations

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

def Lean.Compiler.LCNF.isDeclPublic (env : Environment) (declName : Name) : Bool

Equations

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

def Lean.Compiler.LCNF.setDeclPublic (env : Environment) (declName : Name) : Environment

Equations

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