Package function-def: Definition of function operators and combinators

Information

namefunction-def
version1.13
descriptionDefinition of function operators and combinators
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
requiresbool
showData.Bool
Function

Files

Defined Constants

Theorems

id = λx. x

K = λx y. x

W = λf x. f x x

() = λf g x. f (g x)

C = λf x y. f y x

S = λf g x. f x (g x)

f. surjective f y. x. y = f x

f. injective f x1 x2. f x1 = f x2 x1 = x2

Input Type Operators

Input Constants

Assumptions

() = λp. p = λx.