Skip to content

Consistent naming for auth/view lemmas.

Robbert Krebbers requested to merge robbert/view_auth_frac_rename into master
  1. Use infix _frac for the ●{q} variants. This was already done for the external validity lemmas, but not for those for inclusion and internal validity.
  2. Rename auth_update_core_id into auth_update_frac_alloc. The new name is compatible with the name of the lemma for the view RA, where the concept core_id is not used.
  3. Rename the recently added view_update_alloc_frac into view_update_frac_alloc to be consistent with other lemmas about the placement of _frac.

I have only added item (2) to the CHANGELOG, since the other items concern lemmas that were recently added due to adding the view RA.

@tchajed This might affect your development too.

The complete list of changes for item (1) is:

view_auth_includedN → view_auth_frac_includedN
view_auth_included → view_auth_frac_included
view_both_includedN → view_both_frac_includedN
view_both_included → view_both_frac_included
view_auth_validI → view_auth_frac_validI
auth_auth_includedN → auth_auth_frac_includedN
auth_auth_included → auth_auth_frac_included
auth_both_includedN → auth_both_frac_includedN
auth_both_included → auth_both_frac_included
auth_auth_validI → auth_auth_frac_validI

All of the old names have been repurposed for the without the fraction.

Edited by Robbert Krebbers

Merge request reports