Better names and documentation for proof mode typeclasses
I think the proof mode typeclasses should be documented better, at least the ones that are supposed to have instances added to them. Every such typeclass is essentially a "function", and should be documented as such: What are the inputs, what are the outputs, what's it supposed to do?
Don't expect people know what the Hint Mode
sigils mean, I certainly don't. ;)
I am thinking of something like
(* Input: `P`; Outputs: `Q1`, `Q2`.
Strengthen `P` into a disjunction. Used for `iLeft`, `iRight`. *)
Class FromOr {M} (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P.
(* Input: `P`; Outputs: `Q1`, `Q2`.
Weaken `P` into a disjunction. Used for disjunction elimination patterns. *)
Class IntoOr {M} (P Q1 Q2 : uPred M) := into_or : P ⊢ Q1 ∨ Q2.
For classes like ElimModal
or AddModal
, I have a hard time figuring out what they mean because they are stated in an extremely general way.