Print Sorries Compatibility

This file provides a compatibility shim for #print_sorries_in.

Main declarations

• #print_sorries_in

def «command#print_sorries_in_» : Lean.ParserDescr

#print_sorries_in Foo previously enumerated sorries in a declaration. For now we provide a lightweight compatibility shim that simply logs the requested name so that scripts which call this command continue to elaborate.

Equations

• One or more equations did not get rendered due to their size.