Package list-replicate: The list replicate function

Information

namelist-replicate
version1.36
descriptionThe list replicate function
authorJoe Hurd <joe@gilith.com>
licenseMIT
requiresbool
list-length
list-nth
list-set
natural
set
showData.Bool
Data.List
Number.Natural
Set

Files

Defined Constant

Theorems

x. replicate x 0 = []

x n. length (replicate x n) = n

x n. replicate x (suc n) = x :: replicate x n

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

x n. toSet (replicate x n) = if n = 0 then else insert x

x n y. member y (replicate x n) y = x ¬(n = 0)

Input Type Operators

Input Constants

Assumptions

¬

¬

length [] = 0

toSet [] =

t. t t

p. p

x. ¬(x )

(¬) = λp. p

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

t. (x. t) t

() = λp. p = λx.

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

n. ¬(suc n = 0)

m. m < 0

t. ( t) ¬t

t. t ¬t

() = λp q. p q p

t. (t ) (t )

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

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

h t. length (h :: t) = suc (length t)

m. m = 0 n. m = suc n

l x. member x l x toSet l

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

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

x y. x insert y x = y

h t. toSet (h :: t) = insert h (toSet t)

x s. insert x (insert x s) = insert x s

m n. suc m < suc n m < n

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

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

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

(∃!) = λp. () p x y. p x p y x = y

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

h t n. n < length t nth (h :: t) (suc n) = nth t n

p c x y. p (if c then x else y) (c p x) (¬c p y)