Documentation

Init.Util

Debugging helper functions #

@[never_extract, extern lean_dbg_trace]
def dbgTrace {α : Type u} (s : String) (f : Unitα) :
α
Equations
Instances For
    def dbgTraceVal {α : Type u} [ToString α] (a : α) :
    α
    Equations
    Instances For
      @[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
      Instances For
        @[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
        Instances For
          @[extern lean_dbg_sleep]
          def dbgSleep {α : Type u} (ms : UInt32) (f : Unitα) :
          α
          Equations
          Instances For
            @[never_extract, inline]
            def panicWithPos {α : Type u} [Inhabited α] (modName : String) (line : Nat) (col : Nat) (msg : String) :
            α
            Equations
            Instances For
              @[never_extract, inline]
              def panicWithPosWithDecl {α : Type u} [Inhabited α] (modName : String) (declName : String) (line : Nat) (col : Nat) (msg : String) :
              α
              Equations
              Instances For
                @[extern lean_ptr_addr]
                unsafe opaque ptrAddrUnsafe {α : Type u} (a : α) :
                @[inline]
                unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USizeβ) (h : ∀ (u₁ u₂ : USize), k u₁ = k u₂) :
                β
                Equations
                Instances For
                  @[inline]
                  unsafe def ptrEq {α : Type u_1} (a : α) (b : α) :
                  Equations
                  Instances For
                    unsafe def ptrEqList {α : Type u_1} (as : List α) (bs : List α) :
                    Equations
                    Instances For
                      @[inline]
                      unsafe def withPtrEqUnsafe {α : Type u} (a : α) (b : α) (k : UnitBool) (h : a = bk () = true) :
                      Equations
                      Instances For
                        @[implemented_by withPtrEqUnsafe]
                        def withPtrEq {α : Type u} (a : α) (b : α) (k : UnitBool) (h : a = bk () = true) :
                        Equations
                        Instances For
                          @[inline]
                          def withPtrEqDecEq {α : Type u} (a : α) (b : α) (k : UnitDecidable (a = b)) :
                          Decidable (a = b)

                          withPtrEq for DecidableEq

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[implemented_by withPtrAddrUnsafe]
                            def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USizeβ) (h : ∀ (u₁ u₂ : USize), k u₁ = k u₂) :
                            β
                            Equations
                            Instances For
                              @[inline]
                              def getElem! {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : contidxProp} [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
                              Instances For
                                @[inline]
                                def getElem? {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : contidxProp} [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
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For