mathlib3 documentation

core / init.util

source
def timeit {α : Type u} (s : string) (f : thunk α) :
α

This function has a native implementation that tracks time.

Equations
source
def trace {α : Type u} (s : string) (f : thunk α) :
α

This function has a native implementation that displays the given string in the regular output stream.

Equations
source
meta def trace_val {α : Type u} [has_to_format α] (f : α) :
α
source
def trace_call_stack {α : Type u} (f : thunk α) :
α

This function has a native implementation that shows the VM call stack.

Equations
source
def scope_trace {α : Type u} {line col : ℕ} (f : thunk α) :
α

This function has a native implementation that displays in the given position all trace messages used in f. The arguments line and col are filled by the elaborator.

Equations
source
meta def try_for {α : Type u} (max : ℕ) (f : thunk α) :
option α

This function has a native implementation where the thunk is interrupted if it takes more than 'max' "heartbeats" to compute it. The heartbeat is approx. the maximum number of memory allocations (in thousands) performed by 'f ()'. This is a deterministic way of interrupting long running tasks.

source
meta def try_for_time {α : Type u} (max : ℕ) (f : thunk α) :
option α

This function has a native implementation where the thunk is interrupted if it takes more than max milliseconds to compute it. This is useful due to the variance in the number of heartbeats used by tactics.

source
meta constant undefined_core {α : Sort u} (message : string) :
α

Throws an exception when it is evaluated.

source
meta def undefined {α : Sort u} :
α
source
meta def unchecked_cast {α β : Sort u} :
α → β
source
@[reducible]
def id_tag (tag : unit) {p : Prop} (h : p) :
p

For tactics to tag the proofs they construct. The tag is unit but is intended to be encoded by a constant, e.g. def tagged_proof.ring : unit := ()