Safe Haskell | None |
---|---|
Language | Haskell2010 |
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 `Includes` Integer, uni `Includes` (), uni `Includes` Bool) => term ()
- sum :: (TermLike term TyName Name uni DefaultFun, uni `Includes` Integer) => term ()
- sumr :: (TermLike term TyName Name uni DefaultFun, uni `Includes` Integer) => term ()
- product :: (TermLike term TyName Name uni DefaultFun, uni `Includes` Integer) => term ()
Documentation
listData :: RecursiveType uni fun () Source #
List
as a PLC type.
fix \(list :: * -> *) (a :: *) -> all (r :: *). r -> (a -> list a -> r) -> r
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 `Includes` Integer, uni `Includes` (), uni `Includes` 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 `Includes` Integer) => term () Source #
sum
as a PLC term.
foldList {integer} {integer} addInteger 0
sumr :: (TermLike term TyName Name uni DefaultFun, uni `Includes` Integer) => term () Source #
product :: (TermLike term TyName Name uni DefaultFun, uni `Includes` Integer) => term () Source #
product
as a PLC term.
foldList {integer} {integer} multiplyInteger 1