Sometimes, Armada emits lemmas and/or functions that are never ultimately used by the final proof. This happens because a strategy is generic, and some but not all proofs using that strategy need those elements. The consequence is that the proof takes longer to verify than it needs to.
It would be useful to do a pass over all the elements before emitting them to remove any that aren't needed.
Sometimes, Armada emits lemmas and/or functions that are never ultimately used by the final proof. This happens because a strategy is generic, and some but not all proofs using that strategy need those elements. The consequence is that the proof takes longer to verify than it needs to.
It would be useful to do a pass over all the elements before emitting them to remove any that aren't needed.