Changes between Version 3 and Version 4 of TypeFunctions/TotalFamilies


Ignore:
Timestamp:
Apr 6, 2008 10:29:58 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctions/TotalFamilies

    v3 v4  
    6161}}} 
    6262 
     63=== A rewrite system with total families === 
     64 
     65We denote the rewrite system for `TypeEq` as 
     66{{{ 
     67Et: {TypeEq s s ~ TTrue; TypeEq st ~ TFalse} 
     68}}} 
     69and that of the type-level addition and multiplication as 
     70{{{ 
     71Et: {Z :+ y ~ y; S x :+ y ~ S (x :+ y); _ :+ _ ~ VOID} 
     72      {Z :* y ~ Z; (S x) :* y ~ x :* y :+ y; _ :* _ ~ VOID} 
     73}}} 
     74 
    6375=== Critical examples from the paper === 
    6476