With respect to keeping the language small and simple (C2x charter 6c
and 11) this of course adds a feature. It allows higher-order type
rules (Forall types X, T<X> is a type) which adds to C the remaining
part of the negative fragment of natural deduction for minimal logic
[1], implications being function types and conjunctions implemented
by struct types.
[1]
https://lipn.univ-paris13.fr/~mazza/teaching/ProofTheoryNotes.pdf
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,090 |
| Nodes: | 10 (1 / 9) |
| Uptime: | 156:34:18 |
| Calls: | 13,922 |
| Calls today: | 3 |
| Files: | 187,021 |
| D/L today: |
4,084 files (1,043M bytes) |
| Messages: | 2,457,227 |