Skip to content

Drop `DiagNone` precondition of `lookup_merge` rule of `FinMap` interface.

Robbert Krebbers requested to merge robbert/lookup_merge into master

This fixes issue #94 (closed)

  • Drop DiagNone class.
  • Add merge_proper instance.
  • Simplify lemmas about merge by dropping the DiagNone precondition.
  • Generalize lemmas partial_alter_merge, partial_alter_merge_l, and partial_alter_merge_r.
  • Drop unused merge_assoc' instance, which seems unused, and seems pointless to generalize.

Merge request reports