Rename PParams #216
Rename PParams #216
Conversation
Also adds a check to enactment that all CC members have their term below the max term.
WhatisRT
force-pushed
the
andre/rename-pparams
branch
from
83d01b9 to
5279021
Compare
|
I've added a tiny commit that also closes #219 |
| @@ -72,6 +73,9 @@ record EpochStructure : Set₁ where | |||
| addEpoch : HasAdd Epoch | |||
| addEpoch = record { _+_ = _+ᵉ'_ } | |||
|
|
|||
| Dec-≤ᵉ : ∀ {n m} → Dec (n ≤ᵉ m) | |||
| Dec-≤ᵉ = Decidable²⇒Dec _≤ᵉ?_ | |||
There was a problem hiding this comment.
Something like this should have been part of my type classes PR, but okay...
Also, what's the point of Decidable²⇒Dec? Why don't we use Decidable directly?
Dec-≤ᵉ : ∀ {n m} → Dec (n ≤ᵉ m)
Dec-≤ᵉ {n}{m} = n ≤ᵉ? mThere was a problem hiding this comment.
Yes, but your PR is not even out of WIP yet, and I needed this now so that it can be included in the 0.9 release.
I guess Dec-≤ᵉ could have been implemented directly, but this highlights a general pattern that we could use in the future.
There was a problem hiding this comment.
I'll "unblock" it now.
There was a problem hiding this comment.
Sorry, I didn't realize you were waiting for me to approve the change.
WhatisRT
force-pushed
the
andre/rename-pparams
branch
from
724a15f to
d93d6fb
Compare
|
@williamdemeo I've included your suggestion, could you unblock this PR? |
Description
Renames the PParams to be in line with the CIP & adds a check that new CC members have their term below the maximum.
Checklist