354 | | {{{ |

355 | | cc[[C e1 .. en]] = C_CC e1 .. en , if C_CC exists |

356 | | and arity C = n |

357 | | = , if C_CC exists |

358 | | lam_k $ \x'0 .. x'k -> , and arity C = k + 1 + n |

359 | | (\(x1, .., xn) x(n+1) -> |

360 | | C_CC x1 xn x(n+1) x'0 .. x'k :$ (e1, .. en)) |

361 | | cc[[x::t]] = x_CC , if x_CC exists |

362 | | = to iso<t> x_CC , otherwise |

363 | | cc[[lit]] = lit |

364 | | cc[[e1 e2]] = cc[[e1]] $: cc[e2] |

365 | | cc |

366 | | }}} |

| 354 | We translate terms as follows: |

| 355 | {{{ |

| 356 | cc[[C]] = lam_n C_CC , if C_CC exists |

| 357 | and has arity n |

| 358 | cc[[x::t]] = x_CC , if x_CC exists |

| 359 | = to iso<t> x , otherwise |

| 360 | cc[[lit]] = lit |

| 361 | cc[[e1 e2]] = cc[[e1]] $: cc[e2] |

| 362 | cc[[e1@t]] = cc[[e1]]@t^ |

| 363 | cc[[\x -> e]] = lam_1 $ \x -> cc[e]] |

| 364 | cc[let x = e1 in e2] = let x = cc[[e1]] in cc[[e2]] |

| 365 | cc[[ |

| 366 | }}} |

| 367 | where the family of functions |

| 368 | {{{ |

| 369 | lam_n :: (a1 -> .. -> an -> b) |

| 370 | -> (a1 :-> .. :-> an :-> b) |

| 371 | }}} |

| 372 | turns an `n`-ary function into an `n`-ary closure. (NB: This is not the same as `to iso` for that type, as we do not change the types of the arguments of the function.) |