fix: make A a outParam of Wp and TotalWp#403
Conversation
This reduces the need for type annotations and there should be at most one Wp instance per Expr.
MackieLoeffel
changed the title
|
I don't really have any experience of using |
| wp : A → CoPset → Expr → (Val → PROP) → PROP | ||
|
|
||
| class TotalWP (PROP Expr) (Val : outParam (Type _)) (A : Type _) where | ||
| class TotalWp (PROP Expr) (Val : outParam (Type _)) (A : outParam (Type _)) where |
There was a problem hiding this comment.
The reason why there was a Wp and TotalWP is that, per Iris conventions and Mathlibs naming conventions, both should be spelled out as WP. However, this makes the WP e @ s {{ Q }} notation clash with the typeclass name, which is why I changed it to Wp while I was developing on the file. I think we may be able to fix this by making "WP wpExpr wpPostcond" atomic, so if it cannot be parsed as such it chooses to parse WP as an identifier instead. However, I'm not sure what other ramifications making the whole parser atomic could unchain.
I just wanted to point this out in case we wanted to make the deliberate decision to deviate from normal naming conventions in order to dodge this issue.
There was a problem hiding this comment.
I couldn't find a way to fix it with atomic or something of the sort. I guess this is why Std.Do defines its notation for WP wrapping on the program instead, as wp⟦$x:term⟧ $Q
There was a problem hiding this comment.
Thanks for pointing this out! It seems like you thought about this quite a bit more than I did. I just thought that TotalWP is a typo since TotalWP and Wp seems inconsistent. (I don't know the mathlib naming convention well enough to say whether WP or Wp is the right spelling, both seems fine to me.) @markusdemedeiros What are your thoughts about this?
2 participants
This reduces the need for type annotations and there should be at most one Wp instance per Expr.
@ayhon Please have a look if this makes sense.