Package list-dest: List type destructors

Information

namelist-dest
version1.26
descriptionList type destructors
authorJoe Hurd <joe@gilith.com>
licenseMIT
requiresbool
list-def
list-thm
showData.Bool
Data.List

Files

Defined Constants

Theorems

null []

l. null l l = []

l. case [] (::) l = l

h t. ¬null (h :: t)

h t. head (h :: t) = h

h t. tail (h :: t) = t

b f. case b f [] = b

l. ¬(l = []) head l :: tail l = l

b f h t. case b f (h :: t) = f h t

Input Type Operators

Input Constants

Assumptions

T

¬F T

¬T F

F p. p

(¬) = λp. p F

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

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

t. (T t) t

t. (t T) t

t. F t T

t. T t t

t. (F t) ¬t

t. (t F) ¬t

() = λp q. p q p

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

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

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

x. x = [] a0 a1. x = a0 :: a1

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

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

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

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