Those definitions are the ones which are fully specified by the type, where "any result is acceptable as long as it passes the type checker."
At the moment, the only thing you can do from the dataset is check whether a definition has the Lemma effect. But this seriously underapproximates theorem(-like) definitions. There's plenty of cases where squash is used instead of Lemma etc.
Those definitions are the ones which are fully specified by the type, where "any result is acceptable as long as it passes the type checker."
At the moment, the only thing you can do from the dataset is check whether a definition has the
Lemmaeffect. But this seriously underapproximates theorem(-like) definitions. There's plenty of cases wheresquashis used instead ofLemmaetc.