mathlib documentation

tactic.obviously

The obviously tactic #

This file sets up a tactic called obviously, which is subsequently used throughout the category theory library as an auto_param to discharge easy proof obligations when building structures.

In this file, we set up obviously as a "replacer" tactic, whose implementation can be modified after the fact. Then we set the default implementation to be tidy.

Implementation note #

At present we don't actually take advantage of the replacer mechanism in mathlib. In the past it had been used by an external category theory library which wanted to incorporate rewrite_search as part of obviously.

source
meta def obviously  :
tactic unit

The obviously tactic is a "replaceable" tactic, which means that its meaning is defined by tactics that are defined later with the @[obviously] attribute. It is intended for use with auto_params for structure fields.

source
meta def obviously.attr  :
(user_attribute unit)
source
meta def obviously'  :
tactic unit

The default implementation of obviously discharges any goals which contain sorry in their type using sorry, and then calls tidy.