Post #2945919

@pepper0@aus.social Slightly smaller. 🐞: ```idris module BinList -- Ignore this name mutual record Some (elem : Type) where constructor MkSome head : elem tail : Many elem 0 Many : Type -> Type Many elem = Maybe (Some elem) mutual namespace Some parameters (ab : a -> b) map : Some a -> Some b map (MkSome head tail) = MkSome { head = ab head, tail = map ab tail } parameters (ab : a -> b) map : Many a -> Many b map Nothing = Nothing map (Just s) = Just (map ab s) ``` Fix: ```idris module BinList -- Ignore this name mutual record Some (elem : Type) where constructor MkSome head : elem tail : Many elem 0 Many : Type -> Type Many elem = Maybe (Some elem) mutual namespace Some parameters (ab : a -> b) map : Some a -> Some b map (MkSome head tail) = MkSome { head = ab head, tail = map ab tail } map : (a -> b) -> Many a -> Many b map _ Nothing = Nothing map f (Just s) = Just (map f s) ```