Package list-last: The last list function

Information

namelist-last
version1.53
descriptionThe last list function
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
checksum02d5425ffbdd0eaee8eba7b447ec0cf692b94dbf
requiresbool
list-append
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

l1 l2. last (l1 @ l2) = if null l2 then last l1 else last l2

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

h t l. last (l @ h :: t) = last (h :: t)

External Type Operators

External Constants

Assumptions

null []

p. p

(¬) = λp. p

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

t. (x. t) t

() = λp. p = λx.

t. t

l. [] @ l = l

l. l @ [] = l

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

l1 l2. null (l1 @ l2) null l1 null l2

l h t. (h :: t) @ l = h :: t @ l

p. p [] (h t. p t p (h :: t)) l. p l

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