# Documentation

Lean.Compiler.IR.EmitC

Equations
Instances For
@[inline]
abbrev Lean.IR.EmitC.M (α : Type) :
Equations
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.IR.EmitC.emit {α : Type} [inst : ] (a : α) :
Equations
@[inline]
def Lean.IR.EmitC.emitLn {α : Type} [inst : ] (a : α) :
Equations
• = do
def Lean.IR.EmitC.emitLns {α : Type} [inst : ] (as : List α) :
Equations
Equations
• = match x with | => | x => "lean_box(0)"
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• = >>= Lean.IR.EmitC.emit
Equations
• One or more equations did not get rendered due to their size.
Equations
• = >>= Lean.IR.EmitC.emit
def Lean.IR.EmitC.emitFnDeclAux (decl : Lean.IR.Decl) (cppBaseName : String) (isExternal : Bool) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.IR.EmitC.emitFnDecl (decl : Lean.IR.Decl) (isExternal : Bool) :
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
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.
def Lean.IR.EmitC.isIf (alts : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.IR.EmitC.emitInc (x : Lean.IR.VarId) (n : Nat) (checkRef : Bool) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.IR.EmitC.emitDec (x : Lean.IR.VarId) (n : Nat) (checkRef : Bool) :
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
def Lean.IR.EmitC.emitOffset (n : Nat) (offset : Nat) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.IR.EmitC.emitSSet (x : Lean.IR.VarId) (n : Nat) (offset : Nat) (y : Lean.IR.VarId) (t : Lean.IR.IRType) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
def Lean.IR.EmitC.emitCtorScalarSize (usize : Nat) (ssize : Nat) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.IR.EmitC.emitReuse (z : Lean.IR.VarId) (x : Lean.IR.VarId) (c : Lean.IR.CtorInfo) (updtHeader : Bool) (ys : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.IR.EmitC.emitSProj (z : Lean.IR.VarId) (t : Lean.IR.IRType) (n : Nat) (offset : Nat) (x : Lean.IR.VarId) :
Equations
• One or more equations did not get rendered due to their size.
Equations
def Lean.IR.EmitC.emitSimpleExternalCall (f : String) (ps : ) (ys : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.IR.EmitC.emitExternCall (f : Lean.IR.FunId) (ps : ) (extData : Lean.ExternAttrData) (ys : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• = match x with | => p.x == x | x => false
def Lean.IR.EmitC.overwriteParam (ps : ) (ys : ) :

Given [p_0, ..., p_{n-1}], [y_0, ..., y_{n-1}], representing the assignments

p_0 := y_0,
...
p_{n-1} := y_{n-1}


Return true iff we have (i, j) where j > i, and y_j == p_i. That is, we have

      p_i := y_i,
...
p_j := p_i, -- p_i was overwritten above

Equations
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.IR.EmitC.emitCase (x : Lean.IR.VarId) (xType : Lean.IR.IRType) (alts : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[export lean_ir_emit_c]
def Lean.IR.emitC (env : Lean.Environment) (modName : Lean.Name) :
Equations
• One or more equations did not get rendered due to their size.