Documentation

Init.Util

@[neverExtract, extern lean_dbg_trace]
def dbgTrace {α : Type u} (s : String) (f : Unitα) :
α
Equations
def dbgTraceVal {α : Type u} [inst : ToString α] (a : α) :
α
Equations
@[neverExtract, extern lean_dbg_trace_if_shared]
def dbgTraceIfShared {α : Type u} (s : String) (a : α) :
α
Equations
@[extern lean_dbg_sleep]
def dbgSleep {α : Type u} (ms : UInt32) (f : Unitα) :
α
Equations
@[neverExtract, inline]
def panicWithPos {α : Type u} [inst : Inhabited α] (modName : String) (line : Nat) (col : Nat) (msg : String) :
α
Equations
@[neverExtract, inline]
def panicWithPosWithDecl {α : Type u} [inst : Inhabited α] (modName : String) (declName : String) (line : Nat) (col : Nat) (msg : String) :
α
Equations
@[extern lean_ptr_addr]
unsafe def ptrAddrUnsafe {α : Type u} (a : α) :
Equations
@[inline]
unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USizeβ) (h : ∀ (u₁ u₂ : USize), k u₁ = k u₂) :
β
Equations
@[inline]
unsafe def withPtrEqUnsafe {α : Type u} (a : α) (b : α) (k : UnitBool) (h : a = bk () = true) :
Equations
@[implementedBy withPtrEqUnsafe]
noncomputable def withPtrEq {α : Type u} (a : α) (b : α) (k : UnitBool) (h : a = bk () = true) :
Equations
@[inline]
def withPtrEqDecEq {α : Type u} (a : α) (b : α) (k : (a : Unit) → Decidable (a = b)) :
Decidable (a = b)
Equations

withPtrEq for DecidableEq

@[implementedBy withPtrAddrUnsafe]
noncomputable def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USizeβ) (h : ∀ (u₁ u₂ : USize), k u₁ = k u₂) :
β
Equations