mathlib3 documentation

tactic.print_sorry

Print sorry #

Adds a command #print_sorry_in nm that prints all occurrences of sorry in declarations used in nm, including all intermediate declarations.

Other searches through the environment can be done using tactic.find_all_exprs

source
meta structure tactic.find_all_expr_data  :
Type

Auxiliary data type for tactic.find_all_exprs

source
meta def tactic.find_all_exprs_aux (env : environment) (f : expr → bool) (g : name → bool) :
name → tactic.find_all_expr_data → tactic tactic.find_all_expr_data

Auxiliary declaration for tactic.find_all_exprs.

Traverse all declarations occurring in the declaration with the given name, excluding declarations n such that g n is true (and all their descendants), recording the structure of which declaration depends on which, and whether f e is true on any subexpression e of the declaration.

source
meta def tactic.find_all_exprs (env : environment) (test : expr → bool) (exclude : name → bool) (nm : name) :
tactic (list (name × bool × name_set))

tactic.find_all_exprs env test exclude nm searches for all declarations (transitively) occuring in nm that contain a subexpression e such that test e is true. All declarations n such that exclude n is true (and all their descendants) are ignored.

source
def tactic_doc.command.print_sorry_in  :
tactic_doc_entry

The command

#print_sorry_in nm

prints all declarations that (transitively) occur in the value of declaration nm and depend on sorry. This command assumes that no sorry occurs in mathlib. To find sorry in mathlib, use #eval print_sorry_in `nm ff instead. Example:

def foo1 : false := sorry
def foo2 : false ∧ false := ⟨sorry, foo1⟩
def foo3 : false := foo2.left
def foo4 : true := trivial
def foo5 : true ∧ false := ⟨foo4, foo3⟩
#print_sorry_in foo5

prints

foo5 depends on foo3.
foo3 depends on foo2.
foo2 contains sorry and depends on foo1.
foo1 contains sorry.