Package list-dest: Theory of the list destructors

Information

namelist-dest
version1.13
descriptionTheory of the list destructors
authorJoe Hurd <joe@gilith.com>
licenseMIT
showData.Bool
Data.List

Files

Defined Constants

Theorems

l. null l l = []

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

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

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

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

(null [] T) h t. null (h :: t) F

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

Input Type Operators

Input Constants

Assumptions

T

F p. p

(¬) = λp. p F

() = λP. P ((select) P)

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

x. x = x T

() = λp q. p q p

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

(¬T F) (¬F 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. 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)

t. ((T t) t) ((t T) t) ((F t) ¬t) ((t F) ¬t)

t. (T t t) (t T T) (F t T) (t t T) (t F ¬t)