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 ()

@[never_extract]

def dbgStackTraceIf {α : Type u} (cond : Bool) (f : Unit → α) : α

Print stack trace to stderr before evaluating given closure if cond is true. Currently supported on Linux only.

Equations

• dbgStackTraceIf cond f = if cond = true then dbgStackTrace f else f ()

@[extern lean_dbg_sleep]

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

Equations

• dbgSleep ms f = f ()

@[noinline]

def mkPanicMessage (modName : String) (line col : Nat) (msg : String) : String

Equations

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

@[never_extract, inline]

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

Equations

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

@[noinline]

def mkPanicMessageWithDecl (modName declName : String) (line col : Nat) (msg : String) : String

Equations

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

@[never_extract, inline]

def panicWithPosWithDecl {α : Sort u} [Inhabited α] (modName declName : String) (line 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

Returns the address at which an object is allocated.

This function is unsafe because it can distinguish between definitionally equal values.

@[extern lean_is_exclusive_obj]

unsafe opaque isExclusiveUnsafe {α : Type u} (a : α) : Bool

Returns true if a is an exclusive object.

An object is exclusive if it is single-threaded and its reference counter is 1. This function is unsafe because it can distinguish between definitionally equal values.

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

Compares two objects for pointer equality.

Two objects are pointer-equal if, at runtime, they are allocated at exactly the same address. This function is unsafe because it can distinguish between definitionally equal values.

Equations

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

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

Compares two lists of objects for element-wise pointer equality. Returns true if both lists are the same length and the objects at the corresponding indices of each list are pointer-equal.

Two objects are pointer-equal if, at runtime, they are allocated at exactly the same address. This function is unsafe because it can distinguish between definitionally equal values.

Equations

• ptrEqList [] [] = true
• ptrEqList (a :: as) (b :: bs) = if ptrEq a b = true then ptrEqList as bs else false
• ptrEqList x✝¹ x✝ = false

@[inline]

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

Returns true if a and b are represented by the same pointer at runtime, or k () otherwise.

If k is a function that performs an equality check on a and b, then this operation can be used to short-circuit the equality check for pointer-equal input.

This cannot be wrapped into a safe operation with logical value k () because that would be unsound if α includes computationally irrelevant data like types. Consider the example α := Prop, a := True, b := False, k := fun _ => false. In this case, a = b → k () = true is true, but a and b have the same runtime representation of an erased type, so ptrEq a b is true and this function returns true, even though k () is false.

Users who require a safe version of this function whose logical model is equal to k () must manually check that for their type pointer-equality implies logical equality and then create a specialized version of this function using implemented_by:

namespace MyType

@[inline]
unsafe def withPtrEqUnsafe (a b : MyType) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
  _root_.withPtrEqUnsafe a b k h

-- Safety: `MyType` contains no non-subsingleton erased data
@[implemented_by withPtrEqUnsafe]
def withPtrEq (a b : MyType) (k : Unit → Bool) (_h : a = b → k () = true) : Bool :=
  k ()

end MyType

Equations

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

@[deprecated "See the docstring of `withPtrEqUnsafe`" (since := "2026-09-21")]

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

Equations

• withPtrEq a b k h = withPtrEqUnsafe a b k h

@[inline]

def withPtrEqDecEq {α : Type u} (withPtrEq : (a b : α) → (k : Unit → Bool) → (a = b → k () = true) → Bool) (hw : ∀ (a b : α) (k : Unit → Bool) (h : a = b → k () = true), withPtrEq a b k h = k ()) (a b : α) (k : Unit → Decidable (a = b)) : Decidable (a = b)

Build a DecidableEq instance that short-circuits using withPtrEq where possible. Since the general-purpose withPtrEqUnsafe is unsafe, users need to provide their own withPtrEq function; see the comment on withPtrEqUnsafe.

Equations

• withPtrEqDecEq withPtrEq hw a b k = { decide := withPtrEq a b (fun (x : Unit) => toBoolUsing (k ())) ⋯, reflects_decide := ⋯ }

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