mathlib documentation


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  :

Auxiliary data type for tactic.find_all_exprs

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

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


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