1
{-# OPTIONS --sized-types #-}
10
{-# BUILTIN SIZE Size #-}
11
{-# BUILTIN SIZESUC _^ #-}
12
{-# BUILTIN SIZEINF ∞ #-}
14
data List (A : Set) : {_ : Size} -> Set where
15
[] : {size : Size} -> List A {size ^}
16
_::_ : {size : Size} -> A -> List A {size} -> List A {size ^}
18
map : {A B : Set} -> (A -> B) ->
19
{size : Size} -> List A {size} -> List B {size}
21
map f (x :: xs) = f x :: map f xs
23
data Rose (A : Set) : {_ : Size} -> Set where
24
rose : {size : Size} -> A -> List (Rose A {size}) {∞} -> Rose A {size ^}
27
mapRose : {A B : Set} -> (A -> B) ->
28
{size : Size} -> Rose A {size} -> Rose B {size}
29
mapRose {A} {B} f .{size ^} (rose {size} a l) =
30
rose (f a) (map (\ r -> mapRose {A} {B} f {size} r) l)
33
mapRose : {A B : Set} -> (A -> B) ->
34
{size : Size} -> Rose A {size} -> Rose B {size}
35
mapRose f (rose a l) = rose (f a) (map (mapRose f) l)