[Agda] Wildcards
Guillaume Brunerie
guillaume.brunerie at gmail.com
Sun Mar 25 20:49:58 CEST 2012
2012/3/25 Nils Anders Danielsson <nad at chalmers.se>:
> 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]
But why Agda does not solve the constraints automatically?
It seems to me that Agda could try to simplify the first constraint to
(_89 p q r s ∘ _90 p q r s) = (p ∘ q)
_91 p q r s = (r ∘ s)
and then to
_89 p q r s = p
_90 p q r s = q
_91 p q r s = (r ∘ s)
which solves the first constraint, and then notice that the second is
also satisfied.
Is there a reason Agda does not do this?
Guillaume
More information about the Agda
mailing list