Changes between Version 11 and Version 12 of TypeNats/InductiveDefinitions


Ignore:
Timestamp:
Mar 21, 2012 3:58:06 PM (2 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