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

Information

namelist-replicate
version1.0
description Definitions and theorems about the list replicate function
authorJoe Hurd <joe@gilith.com>
licenseMIT
show Data.Bool
Data.List
Number.Natural
Number.Numeral

Files

Defined Constant

Theorems

n x. length (replicate n x) = n

n x i. i < n nth i (replicate n x) = x

(x. replicate 0 x = []) n x. replicate (suc n) x = x :: replicate n x

Input Type Operators

Input Constants

Assumptions

T

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

t. (x. t) t

() = λP. P = λx. T

x. x = x T

() = λp q. p q p

m. m = 0 n. m = suc n

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

() = λP. q. (x. P x q) q

m n. suc m < suc n m < n

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

length [] = 0 h t. length (h :: t) = suc (length t)

P. P 0 (n. P n P (suc n)) n. P n

e f. fn. fn 0 = e n. fn (suc n) = f (fn n) n

(m. m < 0 F) m n. m < suc n m = n m < n

(h t. nth 0 (h :: t) = h) h t n. nth (suc n) (h :: t) = nth n t

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