[Agda] Boolean And in Pair

[James Wood]

Hi Philippe,

You can see from the source code of `Agda.Builtin.Bool` that it defines
only `Bool`, `true`, and `false`. If you want some operations on
Booleans, you can either define them yourself or get them from a
library, e.g, stdlib's `Data.Bool`. It's best practice to not import
`Agda.Builtin` modules unless you really have to (e.g, if you are
writing your own base library). They may change between versions.

For making your `eq` generic, the simplest thing to do would be to take
as arguments decision procedures for the `fst`s and `snd`s,
respectively. The type should be `{A B : Set} → ((a a′ : A) → Bool) →
((b b′ : B) → Bool) → (ab ab′ : Pair A B) → Bool`.

Additionally, you might want to add `open Pair public` after your
definition of `Pair`, so that you don't have to qualify `fst` and `snd`.
There's an example of this in stdlib's definition of `Σ` (somewhere
around `Data.Product`).

Regards,
James

On 03/05/2020 17:50, Philippe de Rochambeau wrote:
> 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
> 
> 
> openimportAgda.Builtin.Nat
> openimportAgda.Builtin.String
> openimportAgda.Builtin.Bool
> 
> recordPair (A B :Set):Setwhere
>   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)
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>