Package list-concat: Definitions and theorems about the list concat function

Information

namelist-concat
version1.11
description Definitions and theorems about the list concat function
authorJoe Hurd <joe@gilith.com>
licenseMIT
showData.Bool
Data.List

Files

Defined Constant

Theorems

l. null (concat l) all null l

concat [] = [] h t. concat (h :: t) = h @ concat t

Input Type Operators

Input Constants

Assumptions

T

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

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

x. x = x T

() = λp q. p q p

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

l m. null (l @ m) null l null m

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

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)

(P. all P [] T) P h t. all P (h :: t) P h all P t

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