Require ppdWellFormed to imply non-empty updateGroups
#274
Conversation
WhatisRT
force-pushed
the
andre/fix-empty-update-group
branch
from
78a9fec
to
3befddb
Compare
| @@ -156,11 +156,12 @@ HsGovParams : GovParams | |||
| HsGovParams = record | |||
There was a problem hiding this comment.
Why is HsGovParams not called HSGovParams?
None of the other types starts with Hs (i.e. H and lower-case s).
There was a problem hiding this comment.
I didn't touch that part in this PR. Since we'll probably be having a bunch of changes in that file soon I'm not going to bother to fix that inconsistency now.
| @@ -156,11 +156,12 @@ HsGovParams : GovParams | |||
| HsGovParams = record | |||
| { Implementation | |||
There was a problem hiding this comment.
Oh, I wasn't familiar with this syntax. So, does this open up the Implementation module inside the record definition? ...cool!
| .updateGroups → λ _ → ∅ | ||
| .applyUpdate → λ p _ → p | ||
| .ppdWellFormed → λ _ → false | ||
| .ppdWellFormed⇒hasGroup → λ () |
There was a problem hiding this comment.
Question: I see that Agda fills in the proof (λ ()) for us, as the antecedent (false ≡ true) is false. However, I thought we could also prove it explicitly using ⊥-elim, but somehow that's not working for me. I would have thought something like λ f≡t → ⊥-elim f≡t (which is obviously just the function ⊥-elim) would work. The proof λ () works here and I think that means the antecedent is equivalent to ⊥. What am I missing?
There was a problem hiding this comment.
This is simply notation for an empty pattern lambda, so this is almost no magic. If you pattern-match on the proof that false = true, refl doesn't work so you don't need a body in the pattern lambda.
This is very important, otherwise we can't figure out the group and thus the threshold for DReps, making a proposla trivially enactable, with the CC support that is. Related change to the spec: IntersectMBO/formal-ledger-specifications#274
Description
Closes #271. We should probably clean this thing up and expose it in the PDF soon (#273)
Checklist