[Agda] Computation and patterns in called functions

[James Deikun]

On Mon, 2013-01-28 at 17:19 +0100, Nils Anders Danielsson wrote:
> On 2013-01-28 16:40, Francesco Mazzoli wrote:
> > At Mon, 28 Jan 2013 16:24:16 +0100,
> > Nils Anders Danielsson wrote:
> >>     However, it's not quite clear to me what would happen if a duplicated
> >>     right-hand side contained a goal.
> >
> > I don’t get what you mean here.
> 
> Should
> 
>    _≟_ : (x y : Bool) → Dec (x ≡ y)
>    true  ≟ true  = yes refl
>    false ≟ false = yes refl
>    _     ≟ _     = ?
> 
> be expanded into
> 
>    _≟_ : (x y : Bool) → Dec (x ≡ y)
>    true  ≟ true  = yes refl
>    false ≟ false = yes refl
>    true  ≟ false = ?
>    false ≟ true  = ?

Couldn't you do this, using the same meta to represent both occurrences
of the '?'?  The goal shouldn't be able to use anything that isn't in
scope in both lines, so there should be a common telescope to use ...

It does put some constraints on which pass you'd have to do this in,
though.  In particular, after goals are replaced with metas and after
they are counted.