Documentation

List as a PLC type.

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

'[]' as a PLC term.

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

(:) as a PLC term.

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

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')

'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 as a PLC term.

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

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 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 as a PLC term.

foldList {integer} {integer} addInteger 0

product as a PLC term.

foldList {integer} {integer} multiplyInteger 1