Documentation

Lean.Compiler.IR.CompilerM

Instances For
Equations
@[reducible, inline]
Equations
Equations
  • One or more equations did not get rendered due to their size.
@[export lean_ir_log_to_string]
Equations
Equations
@[inline]
Equations
@[export lean_ir_find_env_decl]
def Lean.IR.findEnvDecl (env : Environment) (declName : Name) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
@[export lean_decl_get_sorry_dep]
def Lean.IR.getSorryDep (env : Environment) (declName : Name) :
Equations