Changes between Version 11 and Version 12 of TypeNats/InductiveDefinitions


Ignore:
Timestamp:
Mar 21, 2012 3:58:06 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/InductiveDefinitions

    v11 v12  
    1919the result is typed:  if {{{isZero x}}} returns {{{IsSucc y}}},
    2020then the type checker knows that the type of {{{y}}} is one smaller
    21 then {{{x}}}.
     21than {{{x}}}.
    2222
    2323