search

alexjbest / leaff

Leaff is a diff tool for Lean environments
Apache License 2.0
15 stars 1 forks source link

Identify renamed lemmas #5

Open urkud opened 9 months ago

urkud commented 9 months ago

If a theorem disappeared and a new of the same type appeared, then show as "abc renamed to cde".

alexjbest commented 9 months ago

This should already happen, do you have an explicit example where it doesn't?

urkud commented 9 months ago

You're right, it identifies renames. However, in a more difficult case (renamed, restored the old lemma as a deprecated alias) it randomly reports new or old lemma as added.