mathlib3documentation

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

meta structure tactic.find_all_expr_data  :
• matching_subexpr : bool
• test_passed : bool
• descendants : list
• name_map :
• direct_descendants : name_set

Auxiliary data type for tactic.find_all_exprs

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

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.

meta def tactic.find_all_exprs (env : environment) (test : expr bool) (exclude : name bool) (nm : name) :

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.

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.
`