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 : Unit) => 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

• withPtrEqDecEq a b k = let b_1 := withPtrEq a b (fun (x : Unit) => toBoolUsing (k ())) ⋯; match h : b_1 with | true => isTrue ⋯ | false => isFalse ⋯

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

@[extern lean_runtime_mark_multi_threaded]

def Runtime.markMultiThreaded {α : Sort u_1} (a : α) : α

Marks given value and its object graph closure as multi-threaded if currently marked single-threaded. This will make reference counter updates atomic and thus more costly. It can still be useful to do eagerly when the value will be shared between threads later anyway and there is available time budget to mark it now.

Equations

• Runtime.markMultiThreaded a = a

@[extern lean_runtime_mark_persistent]

def Runtime.markPersistent {α : Sort u_1} (a : α) : α

Marks given value and its object graph closure as persistent. This will remove reference counter updates but prevent the closure from being deallocated until the end of the process! It can still be useful to do eagerly when the value will be marked persistent later anyway and there is available time budget to mark it now or it would be unnecessarily marked multi-threaded in between.

Equations

• Runtime.markPersistent a = a