[Agda] Boolean And in Pair

[Philippe de Rochambeau]

Hi all,
thank you for your suggestions.
I am currently reading through the book entitled The Little Typer.
On p. 17, the authors mention Pairs, which I tried to convert to Agda:

… the normal form of
(Pair
	(car 
		(cons Atom ‘olive))
	(cdr
		(cons ‘oil Atom)))

is 
	(Pair Atom Atom),
and
	(cons ‘ratatouille ‘baguette)
is a
	(Pair Atom Atom).

Apparently, Pair is a type constructor (cf. TLT, p. 30) and is closely associated with what they call The Normal Form.

« Given a type, every expression described by that type has a normal form, which is the most direct way of writing it » , p. 13

Philippe



> Le 3 mai 2020 à 20:00, mechvel at scico.botik.ru a écrit :
> 
> On 2020-05-03 19: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
>> 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)
> 
> 
> If you add
> 
> open import Data.Bool using (_∧_)
> 
> then it is type-checked.
> But I never used "Agda.Builtin" explicitly, and do not know what is the goal.
> 
> Regards,
> 
> ------
> Sergei
> 

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