------------------------------------------------------------------------------------------------------------------------------------------------------------------ ( n : Nat ! data (---------! where zero : Nat ; !-------------! ! Nat : * ) ! suc n : Nat ) ------------------------------------------------------------------------------------------------------------------------------------------------------------------ ( n : Nat ! data !------------! ! Data n : * ) ( s : Data n ! ! ! ( s, t : ! ( s, t : ! ( s : ! ( s : Data n ! ! t : Data (suc n) ! ! Data n ! ! Data n ! ! Data (suc n) ! where (----------------! ; !----------------! ; !------------------! ; (----------! ; !-----------! ; (----------! ; !------------! ; !----------------! ! dz : ! ! ds s : ! ! dlet s t ! ! dzero : ! ! dplus s t ! ! done : ! ! dtimes s t ! ! mu s : Data n ) ! Data (suc n) ) ! Data (suc n) ) ! : Data n ) ! Data n ) ! : Data n ) ! Data n ) ! : Data n ) ------------------------------------------------------------------------------------------------------------------------------------------------------------------ ( n : Nat ! ( as : Tel n ; a : Data n ! data !-----------! where (-----------------! ; !--------------------------! ! Tel n : * ) ! temp : Tel zero ) ! text as a : Tel (suc n) ) ------------------------------------------------------------------------------------------------------------------------------------------------------------------ ( as : Tel n ; a : Data 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 : Data 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 ! ( as : Tel n ! ! ! ! ! ( x : ValT (text as ! f ! ! x : ValT as a ; b : Data n ! ! x : ValT as b ; a : Data n ! ( x : ValT as a ; y : ValT as b ! ! !% (mu f)) ! !-----------------------------! ; !-----------------------------! ; (----------------! ; !--------------------------------! ; !-----------------------! ! inl x : ValT as (dplus a b) ) ! inr x : ValT as (dplus a b) ) ! void : ! ! pair x y : ! ! in x : ValT as (mu f) ) ! ValT as done ) ! ValT as (dtimes a b) ) ------------------------------------------------------------------------------------------------------------------------------------------------------------------ ( as, bs : Tel n ! ( fs : Map as bs ; f : (ValT as a) -> (ValT bs b) ! data !----------------! where (----------------------! ; !--------------------------------------------------! ! Map as bs : * ) ! memp : Map temp temp ) ! mext fs f : Map (text as a) (text bs b) ) ------------------------------------------------------------------------------------------------------------------------------------------------------------------ ( c ; fs : Map as bs ; x : ValT as c ! let !--------------------------------------! ! map c fs x : ValT bs c ) map c fs x <= rec x { map a fs x <= case x { map dz fs (vz x) <= case fs { map dz (mext fs f) (vz x) => vz (f x) } map (ds a) fs (vs x) <= case fs { map (ds a') (mext fs f) (vs x) => vs (map a' fs x) } map (dlet a b) fs (vlet x) => vlet (map b (mext fs (map a fs)) x) map (dplus a b) fs (inl x) => inl (map a fs x) map (dplus a b) fs (inr x) => inr (map b fs x) map done fs void => void map (dtimes a b) fs (pair x y) => pair (map a fs x) (map b fs y) map (mu f) fs (in x) => in (map f (mext fs (map (mu f) fs)) x) } } ------------------------------------------------------------------------------------------------------------------------------------------------------------------