You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, dpdusage prints unused lemmas in an unspecified order that can change unpredictably when including another module in the analysis. In my current use-case (moving a theorem and everything only used to prove this theorem to a separate file) I was interested in the diff between the unused lemmas with and without the extra file. This required a sorted output without the Info line.
A typical invocation of dpdusage might thus look as follows:
Currently,
dpdusage
prints unused lemmas in an unspecified order that can change unpredictably when including another module in the analysis. In my current use-case (moving a theorem and everything only used to prove this theorem to a separate file) I was interested in the diff between the unused lemmas with and without the extra file. This required a sorted output without theInfo
line.A typical invocation of
dpdusage
might thus look as follows:(the use of
.
over:
simplyfies copying lemma names into a "whitelist definition" as a hack until #14 is merged)The text was updated successfully, but these errors were encountered: