------------------------------------------------------------------------------ ( n : Nat ! data (---------! where zero : Nat ; !-------------! ! Nat : * ) ! suc n : Nat ) ------------------------------------------------------------------------------ ( n : Nat ! data !-------------! ! DataP n : * ) where (--------------------! ! dz : DataP (suc n) ) ( a : DataP n ! !----------------------! ! ds a : DataP (suc n) ) ( a : DataP n ; b : DataP (suc n) ! !----------------------------------! ! dlet a b : DataP n ) (-----------------! ! dzero : DataP n ) ( a, b : ! ( a, b : ! ( a : ! ! DataP n ! ! DataP n ! ! DataP (suc n) ! !------------! ; (-----------! ; !------------! ; !-----------------! ! dplus a b ! ! done : ! ! dtimes a b ! ! mu a : DataP n ) ! : DataP n ) ! DataP n ) ! : DataP n ) ------------------------------------------------------------------------------ ( n : Nat ! ( as : Tel n ; a : DataP n ! data !-----------! where (-----------------! ; !---------------------------! ! Tel n : * ) ! temp : Tel zero ) ! text as a : Tel (suc n) ) ------------------------------------------------------------------------------ ( as : Tel n ; a : DataP n ! data !---------------------------! ! ValT as a : * ) ( x : ValT as a ! where !----------------------------! ! vz x : ValT (text as a) dz ) ( as : Tel n ; x : ValT as a ; b : DataP n ! !--------------------------------------------! ! vs x : ValT (text as b) (ds a) ) ( x : ValT (text as a) b ! !-----------------------------! ! vlet x : ValT as (dlet a b) ) ( as : Tel n ; x : ValT as a ; b : DataP n ! !--------------------------------------------! ! inl x : ValT as (dplus a b) ) ( as : Tel n ; x : ValT as b ; a : DataP n ! !--------------------------------------------! ! inr x : ValT as (dplus a b) ) (---------------------! ! void : ValT as done ) ( x : ValT as a ; y : ValT as b ! ( x : ValT (text as (mu f)) f ! !---------------------------------! ; !-----------------------------! ! pair x y : ValT as (dtimes a b) ) ! in x : ValT as (mu f) ) ------------------------------------------------------------------------------ let (----------! ! Data : * ) Data => DataP zero ------------------------------------------------------------------------------ ( d : Data ! let !-----------! ! Val d : * ) Val d => ValT temp d ------------------------------------------------------------------------------ let (------------! ! nat : Data ) nat => mu (dplus done dz) ------------------------------------------------------------------------------ let (--------------! ! nz : Val nat ) nz => in (inl void) ------------------------------------------------------------------------------ ( n : Val nat ! let !------------------! ! ns n : (Val nat) ) ns n => in (inr (vz n)) ------------------------------------------------------------------------------