Fwd: Re: [Agda] commutativity/associativity representation

[Nils Anders Danielsson]

On 2011-02-10 14:41, Permjacov Evgeniy wrote:
> On 02/10/2011 04:32 PM, Nils Anders Danielsson wrote:
>
>>    f₁commutative : ∀ {ℓ} {TF : Set ℓ → Set ℓ} → op₂f₁ TF → Set (suc ℓ)
>>    f₁commutative {TF = TF} op =
>>      ∀ {A} (a b : TF A) → a ⟦ op ⟧ b ≡ b ⟦ op ⟧ a
>>
> sorry, but brief view of tutorials did not give me meaning of { TF =
> TF } here. Could you point me right doc, please?

The syntax { name = pattern } is used for pattern matching on implicit
arguments.

-- 
/NAD