def zip_map

stelliferous@0.0.2.0 · math_sequence.bend:65

import Base

65def zip_map(~Element: Data,~Context: Data,~combine: Context -> Element -> Element -> Element,
66  length: Nat,+context: Context,left: Values(Element,length),right: Values(Element,length)) -> Values(Element,length):
67  match length:
68    case 0n: Unit{}
69    case 1n+rest:
70      Elements{left_head,left_tail} = left
71      Elements{right_head,right_tail} = right
72      Elements{combine(context,left_head,right_head),zip_map(~Element,~Context,~combine,rest,context,left_tail,right_tail)}