Package list-dest: List type destructors

Information

namelist-dest
version1.35
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. ¬null l head l :: tail l = l

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

Input Type Operators

Input Constants

Assumptions

¬

¬

p. p

(¬) = λp. p

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

() = λp. p = λx.

t. ( t) t

t. (t ) t

t. t

t. t t

t. ( t) ¬t

t. (t ) ¬t

() = λp q. p q p

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

() = λ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)

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)