GitLab

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.