Package list-last: The last list function

Information

namelist-last
version1.35
descriptionThe last list function
authorJoe Hurd <joe@gilith.com>
licenseMIT
requiresbool
list-def
list-dest
showData.Bool
Data.List

Files

Defined Constant

Theorems

x. last (x :: []) = x

h t. last (h :: t) = if null t then h else last t

x1 x2 l. last (x1 :: x2 :: l) = last (x2 :: l)

Input Type Operators

Input Constants

Assumptions

null []

p. p

(¬) = λp. p

() = λp. p ((select) p)

t. (x. t) t

() = λp. p = λx.

h t. ¬null (h :: t)

() = λp q. p q p

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

() = λp q. (λf. f p q) = λf. f

() = λp. q. (x. p x q) q

p. (x. y. p x y) y. x. p x (y x)

b f. fn. fn [] = b h t. fn (h :: t) = f h t (fn t)