[Agda] Computation and patterns in called functions

[Nils Anders Danielsson]

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  = ?

?

-- 
/NAD