; more efficient reverse builds a left-fold instead
; (make_left_list a (make_left_list b (make_left_list c empty)) ~~> \f z. f c (f b (f a z))
let reverse = (\make_left_list lst. lst make_left_list empty) (\h t f z. t f (f h z)) in
- ; zip [a;b;c] [x; y; z] ~~> [(a,x);(b,y);(c,z)]
+ ; zip [a;b;c] [x;y;z] ~~> [(a,x);(b,y);(c,z)]
let zip = \left right. (\base build. reverse left build base (\x y. reverse x))
; where base is
(make_pair empty (map (\h u. u h) right))
-->
+
+<!--
+let list_equal =
+ \left right. left
+ ; here's our f
+ (\hd sofar.
+ ; deconstruct our sofar-pair
+ sofar (\might_be_equal right_tail.
+ ; our new sofar
+ make_pair
+ (and (and might_be_equal (not (isempty right_tail))) (eq? hd (head right_tail)))
+ (tail right_tail)
+ ))
+ ; here's our z
+ ; we pass along the fold a pair
+ ; (might_for_all_i_know_still_be_equal?, tail_of_reversed_right)
+ ; when left is empty, the lists are equal if right is empty
+ (make_pair
+ (not (isempty right))
+ (reverse right)
+ )
+ ; when fold is finished, check sofar-pair
+ (\might_be_equal right_tail. and might_be_equal (isempty right_tail))
+-->
+