@@ -98,17 +98,27 @@ instance Functor Binder where
9898 map f (PVar x) = PVar (f x)
9999 map f (PVTy x) = PVTy (f x)
100100
101−total
102−traverse : (Applicative f) => (a -> f b) -> Binder a -> f (Binder b)
103−traverse f (Lam x) = [| Lam (f x) |]
104−traverse f (Pi x) = [| Pi (f x) |]
105−traverse f (Let x y) = [| Let (f x) (f y) |]
106−traverse f (NLet x y) = [| NLet (f x) (f y) |]
107−traverse f (Hole x) = [| Hole (f x) |]
108−traverse f (GHole x) = [| GHole (f x) |]
109−traverse f (Guess x y) = [| Guess (f x) (f y) |]
110−traverse f (PVar x) = [| PVar (f x) |]
111−traverse f (PVTy x) = [| PVTy (f x) |]
101+instance Foldable Binder where
102+ foldr f z (Lam x) = f x z
103+ foldr f z (Pi x) = f x z
104+ foldr f z (Let x y) = f x (f y z)
105+ foldr f z (NLet x y) = f x (f y z)
106+ foldr f z (Hole x) = f x z
107+ foldr f z (GHole x) = f x z
108+ foldr f z (Guess x y) = f x (f y z)
109+ foldr f z (PVar x) = f x z
110+ foldr f z (PVTy x) = f x z
111+
112+instance Traversable Binder where
113+ traverse f (Lam x) = [| Lam (f x) |]
114+ traverse f (Pi x) = [| Pi (f x) |]
115+ traverse f (Let x y) = [| Let (f x) (f y) |]
116+ traverse f (NLet x y) = [| NLet (f x) (f y) |]
117+ traverse f (Hole x) = [| Hole (f x) |]
118+ traverse f (GHole x) = [| GHole (f x) |]
119+ traverse f (Guess x y) = [| Guess (f x) (f y) |]
120+ traverse f (PVar x) = [| PVar (f x) |]
121+ traverse f (PVTy x) = [| PVTy (f x) |]
112122
113123
114124-- | Reflection of the well typed core language