| Copyright | (c) Hisaket VioletRed 2022 |
|---|---|
| License | AGPL-3.0-or-later |
| Maintainer | hisaket@outlook.jp |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Polysemy.FS.Scoped.Internal.MembersProof
Description
Documentation
data MembersProof (es :: EffectRow) (r :: EffectRow) where Source #
Constructors
| EmptyMembersProof :: MembersProof '[] r | |
| MembersProof :: ElemOf e r -> MembersProof es r -> MembersProof (e ': es) r |
membersProof :: Members es r => SList es -> MembersProof es r Source #
membersProofId :: SList l -> MembersProof l l Source #
weakenIdMP :: MembersProof l l -> MembersProof (e ': l) (e ': l) Source #
weakenRightMP :: MembersProof es r -> MembersProof es (e ': r) Source #