Agda-2.3.2.2: test/epic/Prelude/Product.agda
module Prelude.Product where
record _×_ (A B : Set) : Set where
constructor _,_
field
fst : A
snd : B
open _×_ publicmodule Prelude.Product where
record _×_ (A B : Set) : Set where
constructor _,_
field
fst : A
snd : B
open _×_ public