Renaming vprop->slprop + uniform names for each level

[mtzguido]

As discussed today. The slprop types in Pulse.Lib.Core.fsti now look like this:

[@@erasable]
val slprop : Type u#4

[@@erasable]
val slprop2_repr : Type u#3
val cm_slprop2 : CM.cm slprop2_repr
val down2 (p:slprop) : slprop2_repr
val up2 (p:slprop2_repr) : slprop
let is_slprop2 (v:slprop) : prop = up2 (down2 v) == v
val up2_is_slprop2 (p:slprop2_repr) : Lemma (is_slprop2 (up2 p))

[@@erasable]
val slprop1_repr : Type u#2
val cm_slprop1 : CM.cm slprop1_repr
val down1 (p:slprop) : slprop1_repr
val up1 (p:slprop1_repr) : slprop
let is_slprop1 (v:slprop) : prop = up1 (down1 v) == v
val up1_is_slprop1 (p:slprop1_repr) : Lemma (is_slprop1 (up1 p))

let slprop2 = s:slprop { is_slprop2 s }
let slprop1 = s:slprop { is_slprop1 s }

[mtzguido]

The rationale for the naming is that slprop1 can be faithfully turned into and from an slprop1_repr, and the predicate deciding which slprops are slprop1 is called is_slprop1. The down and up functions for slprop1 and down1 and up1. Same for every other number.

Also every slpropN_repr lives in universe N+1.

As a side comment: it doesn't seem we have to expose the cm_ monoids in Core.fsti. Should I delete that?

[mtzguido]

I removed the monoids in Core, and added aliases for the storable slprops.

[nikswamy]

Not exposing the monoids in Core is fine. I added them at one point because I was trying to define a PCM over slprops themselves for use in ConditionVar ... but that didn't work out and these remain unused.

[nikswamy]

Thanks! It's great to clean this up and settle on a systematic naming scheme.