| add : {x : U8,y : U8}# -> U8; | |
| add r = take r2 { x = a } = r : {x : U8,y : U8}# | |
| in take r3 { y = b } = r2 : {x : U8 take,y : U8}# | |
| in if (a : U8) == (0 : U8) : Bool | |
| then b : U8 | |
| else (add[] : {x : U8,y : U8}# | |
| -> U8) ({x = (a : U8) - (1 : U8) : U8 | |
| ,y = (b : U8) + (1 : U8) : U8} : {x : U8 | |
| ,y : U8}#) : U8 | |
| end : U8 | |
| end : U8 | |
| end : U8; |