Init.Util

# Debugging helper functions #

@[never_extract, extern lean_dbg_trace]
def dbgTrace {α : Type u} (s : String) (f : Unitα) :
α
Equations
def dbgTraceVal {α : Type u} [inst : ] (a : α) :
α
Equations
@[never_extract, extern lean_dbg_trace_if_shared]
def dbgTraceIfShared {α : Type u} (s : String) (a : α) :
α

Display the given message if a is shared, that is, RC(a) > 1

Equations
@[never_extract, extern lean_dbg_stack_trace]
def dbgStackTrace {α : Type u} (f : Unitα) :
α

Print stack trace to stderr before evaluating given closure. Currently supported on Linux only.

Equations
@[extern lean_dbg_sleep]
def dbgSleep {α : Type u} (ms : UInt32) (f : Unitα) :
α
Equations
@[never_extract, inline]
def panicWithPos {α : Type u} [inst : ] (modName : String) (line : Nat) (col : Nat) (msg : String) :
α
Equations
@[never_extract, inline]
def panicWithPosWithDecl {α : Type u} [inst : ] (modName : String) (declName : String) (line : Nat) (col : Nat) (msg : String) :
α
Equations
unsafe opaque ptrAddrUnsafe {α : Type u} (a : α) :
@[inline]
unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USizeβ) (h : ∀ (u₁ u₂ : USize), k u₁ = k u₂) :
β
Equations
• = k ()
@[inline]
unsafe def ptrEq {α : Type u_1} (a : α) (b : α) :
Equations
unsafe def ptrEqList {α : Type u_1} (as : List α) (bs : List α) :
Equations
@[inline]
unsafe def withPtrEqUnsafe {α : Type u} (a : α) (b : α) (k : ) (h : a = bk () = true) :
Equations
@[implemented_by withPtrEqUnsafe]
def withPtrEq {α : Type u} (a : α) (b : α) (k : ) (h : a = bk () = true) :
Equations
@[inline]
def withPtrEqDecEq {α : Type u} (a : α) (b : α) (k : UnitDecidable (a = b)) :
Decidable (a = b)

withPtrEq for DecidableEq

Equations
• One or more equations did not get rendered due to their size.
def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USizeβ) (h : ∀ (u₁ u₂ : USize), k u₁ = k u₂) :
β
Equations
@[inline]
def getElem! {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : contidxProp} [inst : GetElem cont idx elem dom] [inst : Inhabited elem] (xs : cont) (i : idx) [inst : Decidable (dom xs i)] :
elem
Equations
• xs[i]! = if h : dom xs i then xs[i] else outOfBounds
@[inline]
def getElem? {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : contidxProp} [inst : GetElem cont idx elem dom] (xs : cont) (i : idx) [inst : Decidable (dom xs i)] :
Option elem
Equations
• xs[i]? = if h : dom xs i then some xs[i] else 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.