Debugging helper functions

@[never_extract, extern lean_dbg_trace]

def dbgTrace {α : Type u} (s : String) (f : Unit → α) : α

Equations

• dbgTrace s f = f ()

def dbgTraceVal {α : Type u} [ToString α] (a : α) : α

Equations

• dbgTraceVal a = dbgTrace (toString a) fun x => a

@[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

• dbgTraceIfShared s a = a

@[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

• dbgStackTrace f = f ()

@[extern lean_dbg_sleep]

def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α

Equations

• dbgSleep ms f = f ()

@[never_extract, inline]

def panicWithPos {α : Type u} [Inhabited α] (modName : String) (line : Nat) (col : Nat) (msg : String) : α

Equations

• panicWithPos modName line col msg = panic (mkPanicMessage modName line col msg)

@[never_extract, inline]

def panicWithPosWithDecl {α : Type u} [Inhabited α] (modName : String) (declName : String) (line : Nat) (col : Nat) (msg : String) : α

Equations

• panicWithPosWithDecl modName declName line col msg = panic (mkPanicMessageWithDecl modName declName line col msg)

@[extern lean_ptr_addr]

unsafe opaque ptrAddrUnsafe {α : Type u} (a : α) : USize

@[inline]

unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ (u₁ u₂ : USize), k u₁ = k u₂) : β

Equations

• withPtrAddrUnsafe a k h = k (ptrAddrUnsafe a)

@[inline]

unsafe def ptrEq {α : Type u_1} (a : α) (b : α) : Bool

Equations

• ptrEq a b = (ptrAddrUnsafe a == ptrAddrUnsafe b)

unsafe def ptrEqList {α : Type u_1} (as : List α) (bs : List α) : Bool

Equations

• ptrEqList x x = match x, x with | [], [] => true | a :: as, b :: bs => if ptrEq a b = true then ptrEqList as bs else false | x, x_1 => false

@[inline]

unsafe def withPtrEqUnsafe {α : Type u} (a : α) (b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool

Equations

• withPtrEqUnsafe a b k h = if ptrEq a b = true then true else k ()

@[implemented_by withPtrEqUnsafe]

def withPtrEq {α : Type u} (a : α) (b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool

Equations

• withPtrEq a b k h = k ()

@[inline]

def withPtrEqDecEq {α : Type u} (a : α) (b : α) (k : Unit → Decidable (a = b)) : Decidable (a = b)

withPtrEq for DecidableEq

Equations

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

@[implemented_by withPtrAddrUnsafe]

def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ (u₁ u₂ : USize), k u₁ = k u₂) : β

Equations

• withPtrAddr a k h = k 0

@[inline]

def getElem! {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem cont idx elem dom] [Inhabited elem] (xs : cont) (i : idx) [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 : cont → idx → Prop} [GetElem cont idx elem dom] (xs : cont) (i : idx) [Decidable (dom xs i)] : Option elem

Equations

• xs[i]? = if h : dom xs i then some xs[i] else none

def «term__[_]_?» : Lean.TrailingParserDescr

Equations

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

def «term__[_]_!» : Lean.TrailingParserDescr

Equations

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