Documentation

Lean.Compiler.NameDemangling

Human-friendly demangling of Lean compiler symbol names, extending Name.demangle with prefix handling, compiler suffix folding, and backtrace line parsing. Called from the C runtime via @[export] for backtrace display.

source
def Lean.Name.Demangle.demangleSymbol (symbol : String) :
Option String
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Name.Demangle.demangleBtLine (line : String) :
    Option String
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For