Documentation

Init.Util

@[neverExtract, extern lean_dbg_trace]

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

α

Equations

dbgTrace s f = f ()

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

α

Equations

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

@[neverExtract, extern lean_dbg_trace_if_shared]

def dbgTraceIfShared {α : Type u} (s : String) (a : α) :

α

Equations

dbgTraceIfShared s a = a

@[extern lean_dbg_sleep]

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

α

Equations

dbgSleep ms f = f ()

@[neverExtract, inline]

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

α

Equations

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

@[neverExtract, inline]

def panicWithPosWithDecl {α : Type u} [inst : 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 def ptrAddrUnsafe {α : Type u} (a : α) :

Equations

ptrAddrUnsafe a = 0

@[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 withPtrEqUnsafe {α : Type u} (a : α) (b : α) (k : Unit → Bool) (h : a = b → k () = true) :

Equations

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

@[implementedBy withPtrEqUnsafe]

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

Equations

withPtrEq a b k h = k ()

@[inline]

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

Decidable (a = b)

Equations

withPtrEqDecEq a b k = let b := withPtrEq a b (fun x => toBoolUsing (k ())) (_ : a = b → toBoolUsing (k ()) = true); match b, (_ : b = b) with | true, h => isTrue (_ : a = b) | false, h => isFalse (_ : ¬a = b)

@[implementedBy withPtrAddrUnsafe]

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

β

Equations

withPtrAddr a k h = k 0