Safe Haskell | Safe-Inferred |
---|---|
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 `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
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