Mercurial > urweb
annotate lib/ur/listPair.ur @ 1508:d236dbf1b3e3
Tutorial proof-reading
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 17 Jul 2011 13:34:41 -0400 |
parents | 1c2f335297b7 |
children | 5c30eea7aa78 |
rev | line source |
---|---|
adamc@850 | 1 fun foldlAbort [a] [b] [c] f = |
adamc@846 | 2 let |
adamc@850 | 3 fun foldlAbort' acc ls1 ls2 = |
adamc@846 | 4 case (ls1, ls2) of |
adamc@846 | 5 ([], []) => Some acc |
adamc@846 | 6 | (x1 :: ls1, x2 :: ls2) => |
adamc@846 | 7 (case f x1 x2 acc of |
adamc@846 | 8 None => None |
adamc@850 | 9 | Some acc' => foldlAbort' acc' ls1 ls2) |
adamc@846 | 10 | _ => None |
adamc@846 | 11 in |
adamc@850 | 12 foldlAbort' |
adamc@846 | 13 end |
adamc@846 | 14 |
adamc@826 | 15 fun mapX [a] [b] [ctx ::: {Unit}] f = |
adamc@801 | 16 let |
adamc@801 | 17 fun mapX' ls1 ls2 = |
adamc@801 | 18 case (ls1, ls2) of |
adamc@801 | 19 ([], []) => <xml/> |
adamc@801 | 20 | (x1 :: ls1, x2 :: ls2) => <xml>{f x1 x2}{mapX' ls1 ls2}</xml> |
adamc@801 | 21 | _ => error <xml>ListPair.mapX: Unequal list lengths</xml> |
adamc@801 | 22 in |
adamc@801 | 23 mapX' |
adamc@801 | 24 end |
adamc@844 | 25 |
adamc@844 | 26 fun all [a] [b] f = |
adamc@844 | 27 let |
adamc@844 | 28 fun all' ls1 ls2 = |
adamc@844 | 29 case (ls1, ls2) of |
adamc@844 | 30 ([], []) => True |
adamc@844 | 31 | (x1 :: ls1, x2 :: ls2) => f x1 x2 && all' ls1 ls2 |
adamc@844 | 32 | _ => False |
adamc@844 | 33 in |
adamc@844 | 34 all' |
adamc@844 | 35 end |