fix subvalue check

This commit is contained in:
Hongrui Fang 2023-04-05 22:22:45 +08:00
parent 9e2b3e0cd3
commit df48c12f6e

View file

@ -176,13 +176,13 @@ psubtractSortedValue = phoistAcyclic $ plam $ \a b ->
# (pfmap # pnegate) # (pfmap # pnegate)
# pto b # pto b
pisPositiveValue :: pisNonNegativeValue ::
forall (kg :: KeyGuarantees) (am :: AmountGuarantees) (s :: S). forall (kg :: KeyGuarantees) (am :: AmountGuarantees) (s :: S).
Term s (PValue kg am :--> PBool) Term s (PValue kg am :--> PBool)
pisPositiveValue = pisNonNegativeValue =
phoistAcyclic $ phoistAcyclic $
plam $ plam $
(AssocMap.pall # (AssocMap.pall # plam (0 #<)) #) (AssocMap.pall # (AssocMap.pall # plam (0 #<=)) #)
. pto . pto
pisSubValueOf :: pisSubValueOf ::
@ -194,7 +194,7 @@ pisSubValueOf ::
:--> PBool :--> PBool
) )
pisSubValueOf = phoistAcyclic $ plam $ \vl vr -> pisSubValueOf = phoistAcyclic $ plam $ \vl vr ->
pisPositiveValue pisNonNegativeValue
#$ psubtractSortedValue #$ psubtractSortedValue
# vl # vl
# vr # vr