Recursive lambdas

[jonaprieto]

f : {A : Type} -> List A -> Pair (List A) Nat;
f := go(acc1 := []; acc2 := 0)@\{
     []        := (acc1, acc2)
   | (x :: xs) := go (x :: acc1) (acc2 + 1) xs
  };

[lukaszcz]

As Jeremy pointed out, it would be more consistent to denote the multiple accumulator arguments as follows:

f : (A : Type) -> List A -> Pair (List A) Nat;
f := go(acc1 := [])(acc2 := 0)@\{
     []        := (acc1, acc2)
   | (x :: xs) := go (x :: acc1) (acc2 + 1) xs
  };

The ; does suggest a pair, which may be confusing.

We could also consider adding optional arguments in general. I opened an issue about them: #1991.