Documentation

[] as a built-in PLC type.

Pattern matching on built-in lists. caseList {a} xs on built-in lists is equivalent to unwrap xs on lists defined in PLC itself (hence why we bind r after xs).

/\(a :: *) -> \(xs : list a) -> /\(r :: *) -> (z : r) (f : a -> list a -> r) ->
    chooseList
        {a}
        {() -> r}
        xs
        (\(u : ()) -> z)
        (\(u : ()) -> f (head {a} xs) (tail {a} xs))
        ()

foldr over built-in lists.

/\(a :: *) (r :: *) -> \(f : a -> r -> r) (z : r) ->
    fix {list a} {r} \(rec : list a -> r) (xs : list a) ->
        caseList {a} 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) ->
        caseList {a} xs {r} z \(x : a) (xs' : list a) -> rec (f z x) xs'

product as a PLC term.

foldList {integer} {integer} multiplyInteger 1