mirror of
https://github.com/github/semantic.git
synced 2025-01-04 13:34:31 +03:00
Rename weaken to weakenSum.
This commit is contained in:
parent
f2eae271fc
commit
d5a35c7904
@ -38,7 +38,7 @@ The data constructors of Sum are not exported.
|
||||
|
||||
module Data.Sum (
|
||||
Sum,
|
||||
weaken,
|
||||
weakenSum,
|
||||
injectSum,
|
||||
projectSum,
|
||||
type(:<),
|
||||
@ -101,8 +101,8 @@ projectSum = unsafeProject (unP (elemNo :: P e r))
|
||||
{-# INLINE projectSum #-}
|
||||
|
||||
|
||||
weaken :: Sum r w -> Sum (any ': r) w
|
||||
weaken (Sum n v) = Sum (n+1) v
|
||||
weakenSum :: Sum r w -> Sum (any ': r) w
|
||||
weakenSum (Sum n v) = Sum (n+1) v
|
||||
|
||||
type (Element t r) = KnownNat (ElemIndex t r)
|
||||
type (t :< r) = Element t r
|
||||
|
Loading…
Reference in New Issue
Block a user