Changes between Version 17 and Version 18 of Commentary/Compiler/TypeType


Ignore:
Timestamp:
Jun 8, 2012 8:25:56 AM (23 months ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/TypeType

    v17 v18  
    88The single data type {{{Type}}} is used to represent 
    99 * Types (possibly of higher kind); e.g. `[Int]`, `Maybe` 
    10  * Coercions; e.g. `trans (sym g) h` 
    11  * Kinds (which classify types and coercions); e.g. `(* -> *)`, `T :=: [Int]` 
     10 * Kinds (which classify types and coercions); e.g. `(* -> *)`, `T :=: [Int]`.  See [wiki:Commentary/Kinds] 
    1211 * Sorts (which classify types); e.g. `TY`, `CO` 
    1312