module Plutarch.List (
PList (PSCons, PSNil),
ptryUncons,
puncons,
pzip,
pfind,
preverse,
pcheckSorted,
pelem,
(#!!),
pelemAt,
pelemAt',
plistEquals,
) where
import Data.Kind (Type)
import GHC.Generics (Generic)
import Plutarch.Builtin.Bool (PBool (PFalse, PTrue), pif, ptrue, (#&&))
import Plutarch.Builtin.Integer (PInteger)
import Plutarch.Internal.Eq (PEq ((#==)))
import Plutarch.Internal.Fix (pfix)
import Plutarch.Internal.Lift (pconstant)
import Plutarch.Internal.ListLike (
PElemConstraint,
PIsListLike,
PListLike,
pcons,
pelimList,
pfoldl,
phead,
pnil,
precList,
ptail,
pzipWith',
)
import Plutarch.Internal.Ord (POrd ((#<), (#<=)))
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
DerivePlutusType (DPTStrat),
PlutusType,
pcon,
pmatch,
)
import Plutarch.Internal.ScottEncoding (
PlutusTypeScott,
)
import Plutarch.Internal.Show (PShow (pshow'), pshowList)
import Plutarch.Internal.Term (
S,
Term,
perror,
phoistAcyclic,
(#),
(#$),
(:-->),
)
import Plutarch.Internal.Trace (ptraceInfo)
import Plutarch.Maybe (PMaybe (PJust, PNothing))
import Plutarch.Pair (PPair (PPair))
data PList (a :: S -> Type) (s :: S)
= PSCons (Term s a) (Term s (PList a))
| PSNil
deriving stock ((forall x. PList a s -> Rep (PList a s) x)
-> (forall x. Rep (PList a s) x -> PList a s)
-> Generic (PList a s)
forall x. Rep (PList a s) x -> PList a s
forall x. PList a s -> Rep (PList a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: S -> Type) (s :: S) x. Rep (PList a s) x -> PList a s
forall (a :: S -> Type) (s :: S) x. PList a s -> Rep (PList a s) x
$cfrom :: forall (a :: S -> Type) (s :: S) x. PList a s -> Rep (PList a s) x
from :: forall x. PList a s -> Rep (PList a s) x
$cto :: forall (a :: S -> Type) (s :: S) x. Rep (PList a s) x -> PList a s
to :: forall x. Rep (PList a s) x -> PList a s
Generic)
deriving anyclass ((forall (s :: S). PList a s -> Term s (PInner (PList a)))
-> (forall (s :: S) (b :: S -> Type).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b)
-> PlutusType (PList a)
forall (s :: S). PList a s -> Term s (PInner (PList a))
forall (s :: S) (b :: S -> Type).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
forall (a :: S -> Type).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: S -> Type).
Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (a :: S -> Type) (s :: S).
PList a s -> Term s (PInner (PList a))
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
$cpcon' :: forall (a :: S -> Type) (s :: S).
PList a s -> Term s (PInner (PList a))
pcon' :: forall (s :: S). PList a s -> Term s (PInner (PList a))
$cpmatch' :: forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
PlutusType)
instance DerivePlutusType (PList a) where
type DPTStrat _ = PlutusTypeScott
instance PShow a => PShow (PList a) where
pshow' :: forall (s :: S). Bool -> Term s (PList a) -> Term s PString
pshow' Bool
_ Term s (PList a)
x = forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
(s :: S).
(PShow a, PIsListLike list a) =>
Term s (list a :--> PString)
pshowList @PList @a Term s (PList a :--> PString) -> Term s (PList a) -> Term s PString
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
x
instance PEq a => PEq (PList a) where
#== :: forall (s :: S).
Term s (PList a) -> Term s (PList a) -> Term s PBool
(#==) Term s (PList a)
xs Term s (PList a)
ys = Term s (PList a :--> (PList a :--> PBool))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
(s :: S).
(PIsListLike list a, PEq a) =>
Term s (list a :--> (list a :--> PBool))
plistEquals Term s (PList a :--> (PList a :--> PBool))
-> Term s (PList a) -> Term s (PList a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
xs Term s (PList a :--> PBool) -> Term s (PList a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
ys
instance PListLike PList where
type PElemConstraint PList _ = ()
pelimList :: forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint PList a =>
(Term s a -> Term s (PList a) -> Term s r)
-> Term s r -> Term s (PList a) -> Term s r
pelimList Term s a -> Term s (PList a) -> Term s r
match_cons Term s r
match_nil Term s (PList a)
ls = Term s (PList a) -> (PList a s -> Term s r) -> Term s r
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PList a)
ls ((PList a s -> Term s r) -> Term s r)
-> (PList a s -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \case
PSCons Term s a
x Term s (PList a)
xs -> Term s a -> Term s (PList a) -> Term s r
match_cons Term s a
x Term s (PList a)
xs
PList a s
PSNil -> Term s r
match_nil
pcons :: forall (a :: S -> Type) (s :: S).
PElemConstraint PList a =>
Term s (a :--> (PList a :--> PList a))
pcons = ClosedTerm (a :--> (PList a :--> PList a))
-> Term s (a :--> (PList a :--> PList a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> (PList a :--> PList a))
-> Term s (a :--> (PList a :--> PList a)))
-> ClosedTerm (a :--> (PList a :--> PList a))
-> Term s (a :--> (PList a :--> PList a))
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s (PList a) -> Term s (PList a))
-> Term s (a :--> (PList a :--> PList a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PList a) -> Term s (PList a))
-> Term s (c :--> (PList a :--> PList a))
plam ((Term s a -> Term s (PList a) -> Term s (PList a))
-> Term s (a :--> (PList a :--> PList a)))
-> (Term s a -> Term s (PList a) -> Term s (PList a))
-> Term s (a :--> (PList a :--> PList a))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s (PList a)
xs -> PList a s -> Term s (PList a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (Term s a -> Term s (PList a) -> PList a s
forall (a :: S -> Type) (s :: S).
Term s a -> Term s (PList a) -> PList a s
PSCons Term s a
x Term s (PList a)
xs)
pnil :: forall (a :: S -> Type) (s :: S).
PElemConstraint PList a =>
Term s (PList a)
pnil = PList a s -> Term s (PList a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PList a s
forall (a :: S -> Type) (s :: S). PList a s
PSNil
ptryUncons ::
PIsListLike list a =>
Term s (list a :--> PPair a (list a))
ptryUncons :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
(s :: S).
PIsListLike list a =>
Term s (list a :--> PPair a (list a))
ptryUncons =
ClosedTerm (list a :--> PPair a (list a))
-> Term s (list a :--> PPair a (list a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> PPair a (list a))
-> Term s (list a :--> PPair a (list a)))
-> ClosedTerm (list a :--> PPair a (list a))
-> Term s (list a :--> PPair a (list a))
forall a b. (a -> b) -> a -> b
$
(Term s (list a) -> Term s (PPair a (list a)))
-> Term s (list a :--> PPair a (list a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PPair a (list a)))
-> Term s (c :--> PPair a (list a))
plam ((Term s (list a) -> Term s (PPair a (list a)))
-> Term s (list a :--> PPair a (list a)))
-> (Term s (list a) -> Term s (PPair a (list a)))
-> Term s (list a :--> PPair a (list a))
forall a b. (a -> b) -> a -> b
$
(Term s a -> Term s (list a) -> Term s (PPair a (list a)))
-> Term s (PPair a (list a))
-> Term s (list a)
-> Term s (PPair a (list a))
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
(r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList (\Term s a
x -> PPair a (list a) s -> Term s (PPair a (list a))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPair a (list a) s -> Term s (PPair a (list a)))
-> (Term s (list a) -> PPair a (list a) s)
-> Term s (list a)
-> Term s (PPair a (list a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s (list a) -> PPair a (list a) s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s a
x) Term s (PPair a (list a))
forall (s :: S) (a :: S -> Type). Term s a
perror
puncons ::
PIsListLike list a =>
Term s (list a :--> PMaybe (PPair a (list a)))
puncons :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
(s :: S).
PIsListLike list a =>
Term s (list a :--> PMaybe (PPair a (list a)))
puncons =
ClosedTerm (list a :--> PMaybe (PPair a (list a)))
-> Term s (list a :--> PMaybe (PPair a (list a)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> PMaybe (PPair a (list a)))
-> Term s (list a :--> PMaybe (PPair a (list a))))
-> ClosedTerm (list a :--> PMaybe (PPair a (list a)))
-> Term s (list a :--> PMaybe (PPair a (list a)))
forall a b. (a -> b) -> a -> b
$
(Term s (list a) -> Term s (PMaybe (PPair a (list a))))
-> Term s (list a :--> PMaybe (PPair a (list a)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PMaybe (PPair a (list a))))
-> Term s (c :--> PMaybe (PPair a (list a)))
plam ((Term s (list a) -> Term s (PMaybe (PPair a (list a))))
-> Term s (list a :--> PMaybe (PPair a (list a))))
-> (Term s (list a) -> Term s (PMaybe (PPair a (list a))))
-> Term s (list a :--> PMaybe (PPair a (list a)))
forall a b. (a -> b) -> a -> b
$
(Term s a -> Term s (list a) -> Term s (PMaybe (PPair a (list a))))
-> Term s (PMaybe (PPair a (list a)))
-> Term s (list a)
-> Term s (PMaybe (PPair a (list a)))
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
(r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList (\Term s a
x -> PMaybe (PPair a (list a)) s -> Term s (PMaybe (PPair a (list a)))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PMaybe (PPair a (list a)) s -> Term s (PMaybe (PPair a (list a))))
-> (Term s (list a) -> PMaybe (PPair a (list a)) s)
-> Term s (list a)
-> Term s (PMaybe (PPair a (list a)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PPair a (list a)) -> PMaybe (PPair a (list a)) s
forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust (Term s (PPair a (list a)) -> PMaybe (PPair a (list a)) s)
-> (Term s (list a) -> Term s (PPair a (list a)))
-> Term s (list a)
-> PMaybe (PPair a (list a)) s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PPair a (list a) s -> Term s (PPair a (list a))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPair a (list a) s -> Term s (PPair a (list a)))
-> (Term s (list a) -> PPair a (list a) s)
-> Term s (list a)
-> Term s (PPair a (list a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s (list a) -> PPair a (list a) s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s a
x) (PMaybe (PPair a (list a)) s -> Term s (PMaybe (PPair a (list a)))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PMaybe (PPair a (list a)) s
forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing)
pzip ::
( PListLike list
, PElemConstraint list a
, PElemConstraint list b
, PElemConstraint list (PPair a b)
) =>
Term s (list a :--> list b :--> list (PPair a b))
pzip :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
(b :: S -> Type) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b,
PElemConstraint list (PPair a b)) =>
Term s (list a :--> (list b :--> list (PPair a b)))
pzip = ClosedTerm (list a :--> (list b :--> list (PPair a b)))
-> Term s (list a :--> (list b :--> list (PPair a b)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> (list b :--> list (PPair a b)))
-> Term s (list a :--> (list b :--> list (PPair a b))))
-> ClosedTerm (list a :--> (list b :--> list (PPair a b)))
-> Term s (list a :--> (list b :--> list (PPair a b)))
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s b -> Term s (PPair a b))
-> Term s (list a :--> (list b :--> list (PPair a b)))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
(b :: S -> Type) (c :: S -> Type) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b,
PElemConstraint list c) =>
(Term s a -> Term s b -> Term s c)
-> Term s (list a :--> (list b :--> list c))
pzipWith' ((Term s a -> Term s b -> Term s (PPair a b))
-> Term s (list a :--> (list b :--> list (PPair a b))))
-> (Term s a -> Term s b -> Term s (PPair a b))
-> Term s (list a :--> (list b :--> list (PPair a b)))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s b
y -> PPair a b s -> Term s (PPair a b)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (Term s a -> Term s b -> PPair a b s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s a
x Term s b
y)
pfind :: PIsListLike l a => Term s ((a :--> PBool) :--> l a :--> PMaybe a)
pfind :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
pfind = ClosedTerm ((a :--> PBool) :--> (l a :--> PMaybe a))
-> Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm ((a :--> PBool) :--> (l a :--> PMaybe a))
-> Term s ((a :--> PBool) :--> (l a :--> PMaybe a)))
-> ClosedTerm ((a :--> PBool) :--> (l a :--> PMaybe a))
-> Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
forall a b. (a -> b) -> a -> b
$
Term
s
((((a :--> PBool) :--> (l a :--> PMaybe a))
:--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
:--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
s
((((a :--> PBool) :--> (l a :--> PMaybe a))
:--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
:--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
-> Term
s
(((a :--> PBool) :--> (l a :--> PMaybe a))
:--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
-> Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
-> Term s (a :--> PBool) -> Term s (l a) -> Term s (PMaybe a))
-> Term
s
(((a :--> PBool) :--> (l a :--> PMaybe a))
:--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c
-> Term s (a :--> PBool) -> Term s (l a) -> Term s (PMaybe a))
-> Term s (c :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
plam ((Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
-> Term s (a :--> PBool) -> Term s (l a) -> Term s (PMaybe a))
-> Term
s
(((a :--> PBool) :--> (l a :--> PMaybe a))
:--> ((a :--> PBool) :--> (l a :--> PMaybe a))))
-> (Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
-> Term s (a :--> PBool) -> Term s (l a) -> Term s (PMaybe a))
-> Term
s
(((a :--> PBool) :--> (l a :--> PMaybe a))
:--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
forall a b. (a -> b) -> a -> b
$ \Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
self Term s (a :--> PBool)
f Term s (l a)
xs ->
(Term s a -> Term s (l a) -> Term s (PMaybe a))
-> Term s (PMaybe a) -> Term s (l a) -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint l a =>
(Term s a -> Term s (l a) -> Term s r)
-> Term s r -> Term s (l a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
(r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList
( \Term s a
y Term s (l a)
ys ->
Term s PBool
-> Term s (PMaybe a) -> Term s (PMaybe a) -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
(Term s (a :--> PBool)
f Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
y)
(PMaybe a s -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PMaybe a s -> Term s (PMaybe a))
-> PMaybe a s -> Term s (PMaybe a)
forall a b. (a -> b) -> a -> b
$ Term s a -> PMaybe a s
forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust Term s a
y)
(Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
self Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
-> Term s (a :--> PBool) -> Term s (l a :--> PMaybe a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> PBool)
f Term s (l a :--> PMaybe a) -> Term s (l a) -> Term s (PMaybe a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
ys)
)
(PMaybe a s -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PMaybe a s
forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing)
Term s (l a)
xs
preverse ::
forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (l a :--> l a)
preverse :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (l a :--> l a)
preverse = ClosedTerm (l a :--> l a) -> Term s (l a :--> l a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (l a :--> l a) -> Term s (l a :--> l a))
-> ClosedTerm (l a :--> l a) -> Term s (l a :--> l a)
forall a b. (a -> b) -> a -> b
$ Term s ((l a :--> (a :--> l a)) :--> (l a :--> (l a :--> l a)))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
(b :: S -> Type).
PIsListLike list a =>
Term s ((b :--> (a :--> b)) :--> (b :--> (list a :--> b)))
pfoldl Term s ((l a :--> (a :--> l a)) :--> (l a :--> (l a :--> l a)))
-> Term s (l a :--> (a :--> l a))
-> Term s (l a :--> (l a :--> l a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (l a) -> Term s a -> Term s (l a))
-> Term s (l a :--> (a :--> l a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a -> Term s (l a))
-> Term s (c :--> (a :--> l a))
plam (\Term s (l a)
xs Term s a
x -> Term s (a :--> (l a :--> l a))
forall (a :: S -> Type) (s :: S).
PElemConstraint l a =>
Term s (a :--> (l a :--> l a))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
(s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s (a :--> (l a :--> l a)) -> Term s a -> Term s (l a :--> l a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s (l a :--> l a) -> Term s (l a) -> Term s (l a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs) Term s (l a :--> (l a :--> l a))
-> Term s (l a) -> Term s (l a :--> l a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
forall (a :: S -> Type) (s :: S).
PElemConstraint l a =>
Term s (l a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
(s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
pcheckSorted ::
forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PIsListLike l a, POrd a) =>
Term s (l a :--> PBool)
pcheckSorted :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PIsListLike l a, POrd a) =>
Term s (l a :--> PBool)
pcheckSorted =
Term
s (((l a :--> PBool) :--> (l a :--> PBool)) :--> (l a :--> PBool))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
s (((l a :--> PBool) :--> (l a :--> PBool)) :--> (l a :--> PBool))
-> Term s ((l a :--> PBool) :--> (l a :--> PBool))
-> Term s (l a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (l a :--> PBool) -> Term s (l a) -> Term s PBool)
-> Term s ((l a :--> PBool) :--> (l a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (l a) -> Term s PBool)
-> Term s (c :--> (l a :--> PBool))
plam ((Term s (l a :--> PBool) -> Term s (l a) -> Term s PBool)
-> Term s ((l a :--> PBool) :--> (l a :--> PBool)))
-> (Term s (l a :--> PBool) -> Term s (l a) -> Term s PBool)
-> Term s ((l a :--> PBool) :--> (l a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (l a :--> PBool)
self Term s (l a)
xs ->
(Term s a -> Term s (l a) -> Term s PBool)
-> Term s PBool -> Term s (l a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint l a =>
(Term s a -> Term s (l a) -> Term s r)
-> Term s r -> Term s (l a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
(r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList
( \Term s a
x1 Term s (l a)
xs ->
(Term s a -> Term s (l a) -> Term s PBool)
-> Term s PBool -> Term s (l a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint l a =>
(Term s a -> Term s (l a) -> Term s r)
-> Term s r -> Term s (l a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
(r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList
(\Term s a
x2 Term s (l a)
_ -> Term s a
x1 Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s a
x2 Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& (Term s (l a :--> PBool)
self Term s (l a :--> PBool) -> Term s (l a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs))
Term s PBool
forall (s :: S). Term s PBool
ptrue
Term s (l a)
xs
)
Term s PBool
forall (s :: S). Term s PBool
ptrue
Term s (l a)
xs
pelem :: (PIsListLike list a, PEq a) => Term s (a :--> list a :--> PBool)
pelem :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
(s :: S).
(PIsListLike list a, PEq a) =>
Term s (a :--> (list a :--> PBool))
pelem =
ClosedTerm (a :--> (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool)))
-> ClosedTerm (a :--> (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool))
forall a b. (a -> b) -> a -> b
$
(Term s a -> Term s (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a :--> PBool))
-> Term s (c :--> (list a :--> PBool))
plam ((Term s a -> Term s (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool)))
-> (Term s a -> Term s (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s a
needle ->
(Term s (list a :--> PBool)
-> Term s a -> Term s (list a) -> Term s PBool)
-> (Term s (list a :--> PBool) -> Term s PBool)
-> Term s (list a :--> PBool)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
(r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList
(\Term s (list a :--> PBool)
self Term s a
x Term s (list a)
xs -> Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
needle) (PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PTrue) (Term s (list a :--> PBool)
self Term s (list a :--> PBool) -> Term s (list a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs))
(\Term s (list a :--> PBool)
_self -> PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse)
plistEquals :: (PIsListLike list a, PEq a) => Term s (list a :--> list a :--> PBool)
plistEquals :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
(s :: S).
(PIsListLike list a, PEq a) =>
Term s (list a :--> (list a :--> PBool))
plistEquals =
ClosedTerm (list a :--> (list a :--> PBool))
-> Term s (list a :--> (list a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> (list a :--> PBool))
-> Term s (list a :--> (list a :--> PBool)))
-> ClosedTerm (list a :--> (list a :--> PBool))
-> Term s (list a :--> (list a :--> PBool))
forall a b. (a -> b) -> a -> b
$
Term
s
(((list a :--> (list a :--> PBool))
:--> (list a :--> (list a :--> PBool)))
:--> (list a :--> (list a :--> PBool)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
s
(((list a :--> (list a :--> PBool))
:--> (list a :--> (list a :--> PBool)))
:--> (list a :--> (list a :--> PBool)))
-> Term
s
((list a :--> (list a :--> PBool))
:--> (list a :--> (list a :--> PBool)))
-> Term s (list a :--> (list a :--> PBool))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (list a :--> (list a :--> PBool))
-> Term s (list a) -> Term s (list a) -> Term s PBool)
-> Term
s
((list a :--> (list a :--> PBool))
:--> (list a :--> (list a :--> PBool)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a) -> Term s (list a) -> Term s PBool)
-> Term s (c :--> (list a :--> (list a :--> PBool)))
plam ((Term s (list a :--> (list a :--> PBool))
-> Term s (list a) -> Term s (list a) -> Term s PBool)
-> Term
s
((list a :--> (list a :--> PBool))
:--> (list a :--> (list a :--> PBool))))
-> (Term s (list a :--> (list a :--> PBool))
-> Term s (list a) -> Term s (list a) -> Term s PBool)
-> Term
s
((list a :--> (list a :--> PBool))
:--> (list a :--> (list a :--> PBool)))
forall a b. (a -> b) -> a -> b
$ \Term s (list a :--> (list a :--> PBool))
self Term s (list a)
xlist Term s (list a)
ylist ->
(Term s a -> Term s (list a) -> Term s PBool)
-> Term s PBool -> Term s (list a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
(r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList
( \Term s a
x Term s (list a)
xs ->
(Term s a -> Term s (list a) -> Term s PBool)
-> Term s PBool -> Term s (list a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
(r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList (\Term s a
y Term s (list a)
ys -> Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
y) (Term s (list a :--> (list a :--> PBool))
self Term s (list a :--> (list a :--> PBool))
-> Term s (list a) -> Term s (list a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs Term s (list a :--> PBool) -> Term s (list a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
ys) (AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False)) (AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False) Term s (list a)
ylist
)
((Term s a -> Term s (list a) -> Term s PBool)
-> Term s PBool -> Term s (list a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
(r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList (\Term s a
_ Term s (list a)
_ -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False) (AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True) Term s (list a)
ylist)
Term s (list a)
xlist
(#!!) :: PIsListLike l a => Term s (l a) -> Term s PInteger -> Term s a
Term s (l a)
l #!! :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (l a) -> Term s PInteger -> Term s a
#!! Term s PInteger
i = Term s (PInteger :--> (l a :--> a))
forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt Term s (PInteger :--> (l a :--> a))
-> Term s PInteger -> Term s (l a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
i Term s (l a :--> a) -> Term s (l a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
l
pelemAt :: PIsListLike l a => Term s (PInteger :--> l a :--> a)
pelemAt :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt = ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a)))
-> ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a))
forall a b. (a -> b) -> a -> b
$
(Term s PInteger -> Term s (l a) -> Term s a)
-> Term s (PInteger :--> (l a :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (l a) -> Term s a)
-> Term s (c :--> (l a :--> a))
plam ((Term s PInteger -> Term s (l a) -> Term s a)
-> Term s (PInteger :--> (l a :--> a)))
-> (Term s PInteger -> Term s (l a) -> Term s a)
-> Term s (PInteger :--> (l a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
n Term s (l a)
xs ->
Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
(Term s PInteger
n Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s PInteger
0)
(Term s PString -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PString -> Term s a -> Term s a
ptraceInfo Term s PString
"pelemAt: negative index" Term s a
forall (s :: S) (a :: S -> Type). Term s a
perror)
(Term s (PInteger :--> (l a :--> a))
forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt' Term s (PInteger :--> (l a :--> a))
-> Term s PInteger -> Term s (l a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
n Term s (l a :--> a) -> Term s (l a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs)
pelemAt' :: PIsListLike l a => Term s (PInteger :--> l a :--> a)
pelemAt' :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt' = ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a)))
-> ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a))
forall a b. (a -> b) -> a -> b
$
Term
s
(((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
:--> (PInteger :--> (l a :--> a)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
s
(((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
:--> (PInteger :--> (l a :--> a)))
-> Term
s ((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
-> Term s (PInteger :--> (l a :--> a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (PInteger :--> (l a :--> a))
-> Term s PInteger -> Term s (l a) -> Term s a)
-> Term
s ((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PInteger -> Term s (l a) -> Term s a)
-> Term s (c :--> (PInteger :--> (l a :--> a)))
plam ((Term s (PInteger :--> (l a :--> a))
-> Term s PInteger -> Term s (l a) -> Term s a)
-> Term
s ((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a))))
-> (Term s (PInteger :--> (l a :--> a))
-> Term s PInteger -> Term s (l a) -> Term s a)
-> Term
s ((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
forall a b. (a -> b) -> a -> b
$ \Term s (PInteger :--> (l a :--> a))
self Term s PInteger
n Term s (l a)
xs ->
Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
(Term s PInteger
n Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
0)
(Term s (l a :--> a)
forall (a :: S -> Type) (s :: S).
PElemConstraint l a =>
Term s (l a :--> a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
(s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s (l a :--> a) -> Term s (l a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs)
(Term s (PInteger :--> (l a :--> a))
self Term s (PInteger :--> (l a :--> a))
-> Term s PInteger -> Term s (l a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
n Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
- Term s PInteger
1) Term s (l a :--> a) -> Term s (l a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (l a :--> l a)
forall (a :: S -> Type) (s :: S).
PElemConstraint l a =>
Term s (l a :--> l a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
(s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail Term s (l a :--> l a) -> Term s (l a) -> Term s (l a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs)