[Agda] Boolean And in Pair

[Philippe de Rochambeau]

Hello,

when I load the following script, I get a « not in scope ∧ » error.
Why is that?
Furthermore, how can I make the eq function generic, whichever the types used in the Pair, as long as the first type is equal to the second?
Many thanks.
Philippe


open import Agda.Builtin.Nat
open import Agda.Builtin.String
open import Agda.Builtin.Bool

record Pair (A B : Set) : Set where
  field
    fst : A
    snd : B

_eq_ : (a : Pair Nat Nat) → (b : Pair Nat Nat) → Bool
a eq b = (Pair.fst a == Pair.fst b) ∧ (Pair.snd a == Pair.snd b)

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200503/5f046e62/attachment.html>