Scrap Your Boilerplate

12 lines of Agda code is verified red-black tree insertion.
12 lines of Java code would be a class declaration with some getters/setters

>>28
More contrived bullshit excuses from you? You'll spew any stupidities if only to never admit that reality doesn't conform to your ignorant pre-conceptions about it? OK, I'll respond but this is the last time:

It was a method to get the effective armor rating. It still is, just that the effective armor is not a field anymore, but a calculated value. But the semantics is the same, thus any and all client code remains working correctly without any adjustments.
Armor rating has to be recalculated every time the unit experiences a hit, so the getter is absolutely the right place for that logic.
The baseArmor is another field that may be used by other methods, e.g. there may be an armor buff that is proportional to the base armor not the effective one.
There is the alternative of keeping the armor field and making all the armor-upgrading and effect-adding methods update it, but that is obviously very brittle and error-prone - if you or the maintainer of your code forget to mutate the armor field in some future magic effect, that will introduce a quiet and hard-to-find bug, as well as making your code harder to understand.