Partial functions don't desugar to total functions with metavariables

[tdidriksen]

Currently, the following only generates a clause for cycle (S n) m:

cycle : Nat -> Nat -> Stream' Nat
&hd cycle n m = n
&tl cycle (S n) m = cycle n m

Resulting in:

cycle : Nat -> Nat -> Stream' Nat
cycle (S n) m = MkStream' (S n) cycle n m

Perhaps two clauses should be generated, such that 'cycle' is desugared to:

cycle : Nat -> Nat -> Stream' Nat
cycle Z m = MkStream' Z ?cycletl
cycle (S n) m = MkStream' (S n) cycle n m

This may or may not be an issue.

[tdidriksen]

On second thought, generating the missing cases might be quite difficult, since we would have to identify all missing cases!