add pisDJust util function

the counterpart of `pisJust`, for type `PMaybeData`
This commit is contained in:
fanghr 2022-04-16 18:27:30 +08:00
parent 7d644c383b
commit 1a17abccd6
No known key found for this signature in database
GPG key ID: 35CD9A71CD5D5870

View file

@ -29,6 +29,7 @@ module Agora.Utils (
pkeysEqual,
pnub,
pisUniq,
pisDJust,
-- * Functions which should (probably) not be upstreamed
anyOutput,
@ -357,6 +358,17 @@ pisUniq =
#&& (self # xs)
)
(const $ pcon PTrue)
-- | Yield True if a given PMaybeData is of form PDJust _.
pisDJust :: Term s (PMaybeData a :--> PBool)
pisDJust = phoistAcyclic $
plam $ \x ->
pmatch
x
( \case
PDJust _ -> pconstant True
_ -> pconstant False
)
--------------------------------------------------------------------------------
{- Functions which should (probably) not be upstreamed