fix subvalue check

This commit is contained in:
Hongrui Fang 2023-04-05 22:22:45 +08:00
parent b4d7c1af42
commit 76b1bdd8bd
No known key found for this signature in database
GPG key ID: F2D0D08AF77AC599

View file

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