Skip to content

Rename `mnat`/`mnat_auth` into `mono_nat`.

Robbert Krebbers requested to merge robbert/mnat_tweaks into master
  • This avoids confusion between mnat and max_nat. The m stands for mono.
  • With _mono added, the _auth suffix in the algebra name no longer makes sense, so I removed it.
  • This makes the names between the logic and the algebra-level liobrary consistent.
  • I also renamed ..._frag into _lb in the algebra-level library so as to make it consistent with the logic-level library.

Furthermore make the order of lemmas consistent and make the versions for the fractions consistent.

/cc @tchajed

Merge request reports