Package natural-numeral: Definitions and theorems about natural number numerals

Information

namenatural-numeral
version1.5
descriptionDefinitions and theorems about natural number numerals
authorJoe Hurd <joe@gilith.com>
licenseMIT
showData.Bool
Number.Natural

Files

Defined Constants

Theorems

1 = suc 0

2 = suc 1

n. bit1 n = suc (bit0 n)

bit0 0 = 0 n. bit0 (suc n) = suc (suc (bit0 n))

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

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