Skip to content

Added IntoPure instance to simplify internal bi equalities into a pure leibniz equality.

Ike Mulder requested to merge snyke7/iris:ike/into_pure_leibniz_equiv into master

For !930, we want to automatically simplify the introduction of a ≡ b : PROP into the pure fact a = b : Prop whenever possible.
This avoids users having to do something like H%leibniz_equiv.

This MR accomplishes that by adding a second IntoPure instance for a ≡ b : PROP, which also makes the simplification happen when using iIntros, on goals like ⊢ a ≡ b -∗ P.

One question I did have: the LeibnizEquiv typeclass currently has Hint Mode ! -, signifying that the type is an input, while the equivalence which is supposed to imply leibniz equality is an output. Should that be Hint Mode ! !, i.e., both are inputs?

Edited by Ike Mulder

Merge request reports