Package list-last: The last list function

Information

namelist-last
version1.29
descriptionThe last list function
authorJoe Hurd <joe@gilith.com>
licenseMIT
requiresbool
set
list-def
list-thm
list-set
list-append
showData.Bool
Data.List
Set

Files

Defined Constant

Theorems

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

l. ¬(l = []) last l toSet l

h t. last (h :: t) = if t = [] then h else last t

h k t. last (h :: k :: t) = last (k :: t)

p q. last (p @ q) = if q = [] then last p else last q

Input Type Operators

Input Constants

Assumptions

T

¬F T

¬T F

t. t t

F p. p

(¬) = λp. p F

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

t. (x. t) t

() = λp. p = λx. T

t. ¬¬t t

t. (T t) t

t. F t F

t. T t t

t. t T t

t. F t T

t. T t t

t. F t t

t. T t T

t. t T T

l. [] @ l = l

t. (F t) ¬t

t. t F ¬t

() = λp q. p q p

t. (t T) (t F)

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

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

h t. ¬(h :: t = [])

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

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

h t. toSet (h :: t) = insert h (toSet t)

() = λp q. r. (p r) (q r) r

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

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

l m. l @ m = [] l = [] m = []

x y s. x insert y s x = y x s

P. P [] (a0 a1. P a1 P (a0 :: a1)) x. P x

p c x y. p (if c then x else y) (c p x) (¬c p y)

NIL' CONS'.
    fn. fn [] = NIL' a0 a1. fn (a0 :: a1) = CONS' a0 a1 (fn a1)