Helper method for creating auxiliary lemmas in the environment.

It uses a cache that maps type to declaration name. The cache is not stored in .olean files. It is useful to make sure the same auxiliary lemma is not created over and over again in the same file.

This method is useful for tactics (e.g., simp) that may perform preprocessing steps to lemmas provided by users. For example, simp preprocessor may convert a lemma into multiple ones.

Instances For