Post #2945916

Replies (1)

• @BoydStephenSmithJr@hachyderm.io 2026-02-14 19:30

  @pepper0@aus.social 🐞: ```idris module BinList mutual record Some (elem : Type) where constructor MkSome head : elem carry : Maybe elem shift : Many (elem, elem) 0 Many : Type -> Type Many elem = Maybe (Some elem) mutual namespace Some parameters (ab : a -> b) mapOnce : (1 _ : Some a) -> Some b mapOnce (MkSome head carry shift) = MkSome { head = ab head, carry = Prelude.map ab carry, shift = map pab shift } where pab : (a, a) -> (b, b) pab (x, y) = (ab x, ab y) map : Some a -> Some b map s = mapOnce s parameters (ab : a -> b) mapOnce : (1 _ : Many a) -> Many b mapOnce Nothing = Nothing mapOnce (Just s) = Just (map ab s) map : Many a -> Many b map m = mapOnce m ``` Fix: ```idris module BinList mutual record Some (elem : Type) where constructor MkSome head : elem carry : Maybe elem shift : Many (elem, elem) 0 Many : Type -> Type Many elem = Maybe (Some elem) mutual namespace Some parameters (ab : a -> b) mapOnce : (1 _ : Some a) -> Some b mapOnce (MkSome head carry shift) = MkSome { head = ab head, carry = Prelude.map ab carry, shift = map pab shift } where pab : (a, a) -> (b, b) pab (x, y) = (ab x, ab y) map : Some a -> Some b map s = mapOnce s mapOnce : (a -> b) -> (1 _ : Many a) -> Many b mapOnce _ Nothing = Nothing mapOnce f (Just s) = Just (map f s) map : (a -> b) -> Many a -> Many b map f m = mapOnce f m ```

  Open ##2945917