Skip to content

Unsilence deprecation warning regarding list lemmas.

Robbert Krebbers requested to merge robbert/deprecate_rev_length into master

I think having our own (direct) version of this two line proof (instead of going via an equivalent to a stdlib def) is less problematic than missing out on other deprecation warnings.

Edited by Robbert Krebbers

Merge request reports