# Documentation

Lean.Compiler.IR.Checker

@[extern c inline "lean_box(LEAN_MAX_CTOR_FIELDS)"]
@[extern c inline "lean_box(LEAN_MAX_CTOR_SCALARS_SIZE)"]
@[extern c inline "lean_box(sizeof(size_t))"]
Instances For
@[inline]
abbrev Lean.IR.Checker.M (α : Type) :
Equations
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.
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 a with | => | x => pure ()
Equations
@[inline]
Equations
• = if (ty₁ == ty₂) = true then else throw "unexpected type '{ty₁}' != '{ty₂}'"
@[inline]
def Lean.IR.Checker.checkType (ty : Lean.IR.IRType) (p : ) (suffix? : optParam () none) :
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.
@[inline]
def Lean.IR.Checker.checkVarType (x : Lean.IR.VarId) (p : ) (suffix? : optParam () none) :
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.
@[inline]
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.checkDecl (decls : ) (decl : Lean.IR.Decl) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.IR.checkDecls (decls : ) :
Equations