Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
Next revisionBoth sides next revision
teaching:cc4101:tareas:2016-2:tarea2 [2016/11/02 00:46] – [P2 - Sistema de Tipos (2.0pt)] fmossoteaching:cc4101:tareas:2016-2:tarea2 [2016/11/02 00:49] – [Recursión] fmosso
Line 121: Line 121:
  
 Funciones definidas con ''def'' pueden ser recursivas y tener más de un argumento. Funciones definidas con ''def'' pueden ser recursivas y tener más de un argumento.
 +
 +<code scheme>
 +(run '{{deftype nat
 +          {O : nat}
 +          {S : {nat -> nat}}}
 +       {def byZero {n : nat} : nat
 +               {match n
 +                 {{case {O} => {O}}
 +                  {case {S {O}} => {byZero {O}}}
 +                  {case {S {S {O}}} => {byZero {S {O}}}}}}}
 +       {byZero {S {S {O}}}}})
 +>"(O) : nat"
 +</code>
  
 <code scheme> <code scheme>