Changes between Version 3 and Version 4 of TypeFunctions/TotalFamilies


Ignore:
Timestamp:
Apr 6, 2008 10:29:58 AM (7 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