def Lean.IR.EmitC.leanMainFn : String

structure Lean.IR.EmitC.Context : Type

• env : Lean.Environment
• modName : Lake.Name
• jpMap : Lean.IR.JPParamsMap
• mainFn : Lean.IR.FunId
• mainParams : Array Lean.IR.Param

@[inline, reducible]

abbrev Lean.IR.EmitC.M (α : Type) : Type

def Lean.IR.EmitC.getEnv : Lean.IR.EmitC.M Lean.Environment

def Lean.IR.EmitC.getModName : Lean.IR.EmitC.M Lake.Name

def Lean.IR.EmitC.getDecl (n : Lake.Name) : Lean.IR.EmitC.M Lean.IR.Decl

@[inline]

def Lean.IR.EmitC.emit {α : Type} [ToString α] (a : α) : Lean.IR.EmitC.M Unit

@[inline]

def Lean.IR.EmitC.emitLn {α : Type} [ToString α] (a : α) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitLns {α : Type} [ToString α] (as : List α) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.argToCString (x : Lean.IR.Arg) : String

def Lean.IR.EmitC.emitArg (x : Lean.IR.Arg) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.toCType : Lean.IR.IRType → String

def Lean.IR.EmitC.throwInvalidExportName {α : Type} (n : Lake.Name) : Lean.IR.EmitC.M α

def Lean.IR.EmitC.toCName (n : Lake.Name) : Lean.IR.EmitC.M String

def Lean.IR.EmitC.emitCName (n : Lake.Name) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.toCInitName (n : Lake.Name) : Lean.IR.EmitC.M String

def Lean.IR.EmitC.emitCInitName (n : Lake.Name) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitFnDeclAux (decl : Lean.IR.Decl) (cppBaseName : String) (isExternal : Bool) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitFnDecl (decl : Lean.IR.Decl) (isExternal : Bool) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitExternDeclAux (decl : Lean.IR.Decl) (cNameStr : String) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitFnDecls : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitMainFn : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.hasMainFn : Lean.IR.EmitC.M Bool

def Lean.IR.EmitC.emitMainFnIfNeeded : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitFileHeader : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitFileFooter : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.throwUnknownVar {α : Type} (x : Lean.IR.VarId) : Lean.IR.EmitC.M α

def Lean.IR.EmitC.getJPParams (j : Lean.IR.JoinPointId) : Lean.IR.EmitC.M (Array Lean.IR.Param)

def Lean.IR.EmitC.declareVar (x : Lean.IR.VarId) (t : Lean.IR.IRType) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.declareParams (ps : Array Lean.IR.Param) : Lean.IR.EmitC.M Unit

partial def Lean.IR.EmitC.declareVars : Lean.IR.FnBody → Bool → Lean.IR.EmitC.M Bool

def Lean.IR.EmitC.emitTag (x : Lean.IR.VarId) (xType : Lean.IR.IRType) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.isIf (alts : Array Lean.IR.Alt) : Option (Nat × Lean.IR.FnBody × Lean.IR.FnBody)

def Lean.IR.EmitC.emitInc (x : Lean.IR.VarId) (n : Nat) (checkRef : Bool) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitDec (x : Lean.IR.VarId) (n : Nat) (checkRef : Bool) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitDel (x : Lean.IR.VarId) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitSetTag (x : Lean.IR.VarId) (i : Nat) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitSet (x : Lean.IR.VarId) (i : Nat) (y : Lean.IR.Arg) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitOffset (n : Nat) (offset : Nat) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitUSet (x : Lean.IR.VarId) (n : Nat) (y : Lean.IR.VarId) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitSSet (x : Lean.IR.VarId) (n : Nat) (offset : Nat) (y : Lean.IR.VarId) (t : Lean.IR.IRType) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitJmp (j : Lean.IR.JoinPointId) (xs : Array Lean.IR.Arg) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitLhs (z : Lean.IR.VarId) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitArgs (ys : Array Lean.IR.Arg) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitCtorScalarSize (usize : Nat) (ssize : Nat) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitAllocCtor (c : Lean.IR.CtorInfo) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitCtorSetArgs (z : Lean.IR.VarId) (ys : Array Lean.IR.Arg) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitCtor (z : Lean.IR.VarId) (c : Lean.IR.CtorInfo) (ys : Array Lean.IR.Arg) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitReset (z : Lean.IR.VarId) (n : Nat) (x : Lean.IR.VarId) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitReuse (z : Lean.IR.VarId) (x : Lean.IR.VarId) (c : Lean.IR.CtorInfo) (updtHeader : Bool) (ys : Array Lean.IR.Arg) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitProj (z : Lean.IR.VarId) (i : Nat) (x : Lean.IR.VarId) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitUProj (z : Lean.IR.VarId) (i : Nat) (x : Lean.IR.VarId) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitSProj (z : Lean.IR.VarId) (t : Lean.IR.IRType) (n : Nat) (offset : Nat) (x : Lean.IR.VarId) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.toStringArgs (ys : Array Lean.IR.Arg) : List String

def Lean.IR.EmitC.emitSimpleExternalCall (f : String) (ps : Array Lean.IR.Param) (ys : Array Lean.IR.Arg) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitExternCall (f : Lean.IR.FunId) (ps : Array Lean.IR.Param) (extData : Lean.ExternAttrData) (ys : Array Lean.IR.Arg) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitFullApp (z : Lean.IR.VarId) (f : Lean.IR.FunId) (ys : Array Lean.IR.Arg) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitPartialApp (z : Lean.IR.VarId) (f : Lean.IR.FunId) (ys : Array Lean.IR.Arg) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitApp (z : Lean.IR.VarId) (f : Lean.IR.VarId) (ys : Array Lean.IR.Arg) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitBoxFn (xType : Lean.IR.IRType) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitBox (z : Lean.IR.VarId) (x : Lean.IR.VarId) (xType : Lean.IR.IRType) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitUnbox (z : Lean.IR.VarId) (t : Lean.IR.IRType) (x : Lean.IR.VarId) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitIsShared (z : Lean.IR.VarId) (x : Lean.IR.VarId) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.toHexDigit (c : Nat) : String

def Lean.IR.EmitC.quoteString (s : String) : String

def Lean.IR.EmitC.emitNumLit (t : Lean.IR.IRType) (v : Nat) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitLit (z : Lean.IR.VarId) (t : Lean.IR.IRType) (v : Lean.IR.LitVal) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitVDecl (z : Lean.IR.VarId) (t : Lean.IR.IRType) (v : Lean.IR.Expr) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.isTailCall (x : Lean.IR.VarId) (v : Lean.IR.Expr) (b : Lean.IR.FnBody) : Lean.IR.EmitC.M Bool

def Lean.IR.EmitC.paramEqArg (p : Lean.IR.Param) (x : Lean.IR.Arg) : Bool

def Lean.IR.EmitC.overwriteParam (ps : Array Lean.IR.Param) (ys : Array Lean.IR.Arg) : Bool

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

def Lean.IR.EmitC.emitTailCall (v : Lean.IR.Expr) : Lean.IR.EmitC.M Unit

partial def Lean.IR.EmitC.emitIf (x : Lean.IR.VarId) (xType : Lean.IR.IRType) (tag : Nat) (t : Lean.IR.FnBody) (e : Lean.IR.FnBody) : Lean.IR.EmitC.M Unit

partial def Lean.IR.EmitC.emitCase (x : Lean.IR.VarId) (xType : Lean.IR.IRType) (alts : Array Lean.IR.Alt) : Lean.IR.EmitC.M Unit

partial def Lean.IR.EmitC.emitBlock (b : Lean.IR.FnBody) : Lean.IR.EmitC.M Unit

partial def Lean.IR.EmitC.emitJPs : Lean.IR.FnBody → Lean.IR.EmitC.M Unit

partial def Lean.IR.EmitC.emitFnBody (b : Lean.IR.FnBody) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitDeclAux (d : Lean.IR.Decl) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitDecl (d : Lean.IR.Decl) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitFns : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitMarkPersistent (d : Lean.IR.Decl) (n : Lake.Name) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitDeclInit (d : Lean.IR.Decl) : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.emitInitFn : Lean.IR.EmitC.M Unit

def Lean.IR.EmitC.main : Lean.IR.EmitC.M Unit

@[export lean_ir_emit_c]

def Lean.IR.emitC (env : Lean.Environment) (modName : Lake.Name) : Except String String