Package list-nth-def: list-nth-def

Information

namelist-nth-def
version1.12
descriptionlist-nth-def
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-07-25
showData.Bool

Files

Defined Constant

Theorem

(h t. Data.List.nth 0 (Data.List.:: h t) = h)
  h t n.
    Number.Natural.< n (Data.List.length t)
    Data.List.nth (Number.Natural.suc n) (Data.List.:: h t) =
    Data.List.nth n t

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

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

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

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

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

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

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

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