Documentation

The anonymous constructor ⟨e, ...⟩ is equivalent to c e ... if the expected type is an inductive type with a single constructor c. If more terms are given than c has parameters, the remaining arguments are turned into a new anonymous constructor application. For example, ⟨a, b, c⟩ : α × (β × γ) is equivalent to ⟨a, ⟨b, c⟩⟩.

panic! msg formally evaluates to @Inhabited.default α if the expected type α implements Inhabited. At runtime, msg and the file position are printed to stderr unless the C function lean_set_panic_messages(false) has been executed before. If the C function lean_set_exit_on_panic(true) has been executed before, the process is then aborted.

A shorthand for panic! "unreachable code has been reached".

assert! cond panics if cond evaluates to false.

dbg_trace e; body evaluates to body and prints e (which can be an interpolated string literal) to stderr. It should only be used for debugging.

A temporary placeholder for a missing proof or value.

Return syntax Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))

Return some if succeeded expanding · notation occurring in the given syntax. Otherwise, return none. Examples:

• · + 1 => fun _a_1 => _a_1 + 1
• f · · b => fun _a_1 _a_2 => f _a_1 _a_2 b

Helper method for elaborating terms such as (.+.) where a constant name is expected. This method is usually used to implement tactics that function names as arguments (e.g., simp).

h ▸ e is a macro built on top of Eq.subst and Eq.symm definitions. Given h : a = b and e : p a, the term h ▸ e has type p b. You can also view h ▸ e as a "type casting" operation where you change the type of e by using h. See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lean" for additional information.