| Specware 4.1 Language Manual | ||
|---|---|---|
| Prev | Appendix B. Inbuilts and Base Libraries | |
type Injective(a,b) = ((a -> b) | injective?)
type Surjective(a,b) = ((a -> b) | surjective?)
type Bijective(a,b) = ((a -> b) | bijective?)
| Name | Fixity | Type | Description |
|---|---|---|---|
| id | [a] a -> a | identity function | |
| o | L 24 | [a,b,c] (b -> c) * (a -> b) -> (a -> c) | function composition |
| injective? | [a,b] (a -> b) -> Boolean | injectivity predicate; non-constructive | |
| surjective? | [a,b] (a -> b) -> Boolean | surjectivity predicate; non-constructive | |
| bijective? | [a,b] (a -> b) -> Boolean | bijectivity predicate; non-constructive | |
| inverse | [a,b] Bijective(a,b) -> Bijective(b,a) | inverts bijective function; non-constructive |