Safe Haskell	Safe-Inferred
Language	Haskell2010

PlutusCore.StdLib.Data.ScottList

Description

list and related functions.

Synopsis

listData :: RecursiveType uni fun ()
listTy :: Type TyName uni ()
nil :: TermLike term TyName Name uni fun => term ()
cons :: TermLike term TyName Name uni fun => term ()
foldrList :: TermLike term TyName Name uni fun => term ()
foldList :: TermLike term TyName Name uni fun => term ()
map :: TermLike term TyName Name uni fun => term ()
reverse :: TermLike term TyName Name uni fun => term ()
enumFromTo :: (TermLike term TyName Name uni DefaultFun, uni `HasTypeAndTermLevel` Integer, uni `HasTypeAndTermLevel` (), uni `HasTypeAndTermLevel` Bool) => term ()
sum :: (TermLike term TyName Name uni DefaultFun, uni `HasTypeAndTermLevel` Integer) => term ()
sumr :: (TermLike term TyName Name uni DefaultFun, uni `HasTypeAndTermLevel` Integer) => term ()
product :: (TermLike term TyName Name uni DefaultFun, uni `HasTypeAndTermLevel` Integer) => term ()

Documentation

listData :: RecursiveType uni fun () Source #

List as a PLC type.

fix \(list :: * -> *) (a :: *) -> all (r :: *). r -> (a -> list a -> r) -> r

listTy :: Type TyName uni () Source #

nil :: TermLike term TyName Name uni fun => term () Source #

'[]' as a PLC term.

 /\(a :: *) -> wrapList [a] /\(r :: *) -> \(z : r) (f : a -> list a -> r) -> z)

cons :: TermLike term TyName Name uni fun => term () Source #

(:) as a PLC term.

/\(a :: *) -> \(x : a) (xs : list a) ->
    wrapList [a] /\(r :: *) -> \(z : r) (f : a -> list a -> r) -> f x xs

foldrList :: TermLike term TyName Name uni fun => term () Source #

foldrList as a PLC term.

/\(a :: *) (r :: *) -> \(f : a -> r -> r) (z : r) ->
    fix {list a} {r} \(rec : list a -> r) (xs : list a) ->
        unwrap xs {r} z \(x : a) (xs' : list a) -> f x (rec xs')

foldList :: TermLike term TyName Name uni fun => term () Source #

'foldl'' as a PLC term.

/\(a :: *) (r :: *) -> \(f : r -> a -> r) ->
    fix {r} {list a -> r} \(rec : r -> list a -> r) (z : r) (xs : list a) ->
        unwrap xs {r} z \(x : a) (xs' : list a) -> rec (f z x) xs'

map :: TermLike term TyName Name uni fun => term () Source #

map as a PLC term.

/\(a :: *) (b :: *) -> \(f : a -> b) ->
    foldrList {a} {list b} (\(x : a) -> cons {b} (f x)) (nil {b})

reverse :: TermLike term TyName Name uni fun => term () Source #

reverse as a PLC term.

/\(a :: *) -> \(xs : list a) ->
    foldList {a} {list a} (\(r : list a) (x : a) -> cons {a} x r) (nil {a})

enumFromTo :: (TermLike term TyName Name uni DefaultFun, uni `HasTypeAndTermLevel` Integer, uni `HasTypeAndTermLevel` (), uni `HasTypeAndTermLevel` Bool) => term () Source #

enumFromTo as a PLC term

\(n m : integer) ->
    fix {integer} {list (integer)}
        (\(rec : integer -> list (integer)) (n' : integer) ->
            ifThenElse {list (integer)}
                (lessThanEqualsInteger n' m)
                (cons {integer} n' (rec (succInteger n')))
                (nil {integer}))
        n

sum :: (TermLike term TyName Name uni DefaultFun, uni `HasTypeAndTermLevel` Integer) => term () Source #

sum as a PLC term.

foldList {integer} {integer} addInteger 0

sumr :: (TermLike term TyName Name uni DefaultFun, uni `HasTypeAndTermLevel` Integer) => term () Source #

product :: (TermLike term TyName Name uni DefaultFun, uni `HasTypeAndTermLevel` Integer) => term () Source #

product as a PLC term.

foldList {integer} {integer} multiplyInteger 1