source
def Lean.Compiler.LCNF.isCompilerRelevantMData (_mdata : MData) :
Bool

Return `true` if `mdata` should be preserved. Right now, we don't preserve any `MData`, but this may change in the future when we add support for debugging information

Equations

- Lean.Compiler.LCNF.isCompilerRelevantMData _mdata = false

Instances For

source
def Lean.Compiler.LCNF.isLcCast? (e : Expr) :
Option Expr

Return `true` if `e` is a `lcCast` application.

Equations

- Lean.Compiler.LCNF.isLcCast? e = if e.isAppOfArity `lcCast 3 = true then some e.appArg! else none

Instances For

source
structure Lean.Compiler.LCNF.CasesInfo :
Type

Store information about `casesOn` declarations.

We treat them uniformly in the code generator.

- declName : Name
- arity : Nat
- numParams : Nat
- discrPos : Nat
- altsRange : Std.Rco Nat
- altNumParams : Array Nat
- motivePos : Nat

Instances For

source
def Lean.Compiler.LCNF.CasesInfo.numAlts (c : CasesInfo) :
Nat
Equations

- c.numAlts = c.altNumParams.size

Instances For

source
def Lean.Compiler.LCNF.getCasesInfo? (declName : Name) :
CoreM (Option CasesInfo)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Compiler.LCNF.isCasesApp? (e : Expr) :
CoreM (Option CasesInfo)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Compiler.LCNF.getCtorArity? (declName : Name) :
CoreM (Option Nat)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Compiler.LCNF.builtinRuntimeTypes :
Array Name

List of types that have builtin runtime support

Equations

- Lean.Compiler.LCNF.builtinRuntimeTypes = #[`String, `UInt8, `UInt16, `UInt32, `UInt64, `USize, `Float, `Float32, `Thunk, `Task, `Array, `ByteArray, `FloatArray, `Nat, `Int]

Instances For

source
def Lean.Compiler.LCNF.isRuntimeBuiltinType (declName : Name) :
Bool

Return `true` iff `declName` is the name of a type with builtin support in the runtime.

Equations

- Lean.Compiler.LCNF.isRuntimeBuiltinType declName = Lean.Compiler.LCNF.builtinRuntimeTypes.contains declName

Instances For