| Specware 4.0 Language Manual | ||
|---|---|---|
| Prev | Appendix B. Base Libraries | |
sort Injective(a,b) = ((a -> b) | injective?)
sort Surjective(a,b) = ((a -> b) | surjective?)
sort Bijective(a,b) = ((a -> b) | bijective?)
| Name | Fixity | Sort | Description |
|---|---|---|---|
| id | fa(a) a -> a | identity function | |
| o | infixl 24 | fa(a,b,c) (b -> c) * (a -> b) -> (a -> c) | function composition |
| injective? | fa(a,b) (a -> b) -> Boolean | injectivity predicate; non-constructive | |
| surjective? | fa(a,b) (a -> b) -> Boolean | surjectivity predicate; non-constructive | |
| bijective? | fa(a,b) (a -> b) -> Boolean | bijectivity predicate; non-constructive | |
| inverse | fa(a,b) Bijective(a,b) -> Bijective(b,a) | inverts bijective function; non-constructive |