Commit 2023-04-07 11:11 dc37f26f
View on Github →chore: rename castLT
(#3320)
From #2450:
castSucc_cast_lt
is misnamed, it should becastSucc_castLt
. I wonder why mathport can't align it. This PR goes one step further and renamescastLt
tocastLT
everywhere, per https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/!4.233320/near/347567570.