[Agda] Wildcards

[Nils Anders Danielsson]

On 2012-03-25 19:33, Guillaume Brunerie wrote:
> My impression is that if you try to unify the types of [assoc] and
> [big-assoc], you automatically find the three arguments of [assoc], so
> I do not understand why the wildcards are not sufficient.

You can ask Agda to display unsolved constraints (using a menu entry or
C-c C-=). In your case:

   [112] ((_89 p q r s ∘ _90 p q r s) ∘ _91 p q r s) = ((p ∘ q) ∘ (r ∘ s)) : .x ≡ .u
   [112] (_89 p q r s ∘ (_90 p q r s ∘ _91 p q r s)) = (p ∘ (q ∘ (r ∘ s))) : .x ≡ .u
   _92 := λ {.A} {.x} {.y} {.z} {.t} {.u} p q r s →
     assoc (_89 p q r s) (_90 p q r s) (_91 p q r s) [blocked by problem 112]

-- 
/NAD