Documentation

Lean.Compiler.IR.EmitC

structure Lean.IR.EmitC.Context :
Type
@[inline]
abbrev Lean.IR.EmitC.M (α : Type) :
Type
Equations
Equations
@[inline]
def Lean.IR.EmitC.emit {α : Type} [inst : ToString α] (a : α) :
Equations
@[inline]
def Lean.IR.EmitC.emitLn {α : Type} [inst : ToString α] (a : α) :
Equations
def Lean.IR.EmitC.emitLns {α : Type} [inst : ToString α] (as : List α) :
Equations
Equations
Equations
def Lean.IR.EmitC.emitFnDeclAux (decl : Lean.IR.Decl) (cppBaseName : String) (isExternal : Bool) :
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations