<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Thanks, Oleg!<div class="">Is this correct?:</div><div class=""><br class=""></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class=""><font face="Menlo" class="">55 record _×_ (A : Set) (B : Set) : Set where</font></div></div><div class=""><div class=""><font face="Menlo" class="">56 field</font></div></div><div class=""><div class=""><font face="Menlo" class="">57 fst : A</font></div></div><div class=""><div class=""><font face="Menlo" class="">58 snd : B</font></div></div><div class=""><div class=""><font face="Menlo" class="">59 </font></div></div><div class=""><div class=""><font face="Menlo" class="">60 _,_ : ∀ {A B : Set} A → B → (A × B)</font></div></div><div class=""><div class=""><font face="Menlo" class="">61 x , y = record {fst = x; snd = y}</font></div></div></blockquote><div class=""><div class=""><br class=""></div><div class="">It seems to work, in general, but is giving me the following error, re: my Functor instance:</div><div class=""><br class=""></div></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class=""><div class=""><font face="Menlo" class="">###.agda:112,3-36</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">Could not parse the left-hand side</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">fmap ⦃ ProductFunctor ⦄ f (x , y)</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">Operators used in the grammar:</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class=""> , (infix operator, level 20) [_,_ (###.agda:60,1-4)]</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">when scope checking the left-hand side</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">fmap ⦃ ProductFunctor ⦄ f (x , y) in the definition of</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">ProductFunctor</font></div></div></div></blockquote><div class=""><div class=""><br class=""></div><div class="">For reference, here is that Functor instance:</div><div class=""><br class=""></div></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class=""><div class=""><font face="Menlo" class="">110 instance</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">111 ProductFunctor : ∀ {A : Set} → Functor (_× A)</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">112 fmap {{ProductFunctor}} f (x , y) = (f x , y)</font></div></div></div></blockquote><div class=""><div class=""><br class=""></div><div class="">Thanks,</div><div class="">-db</div><div class=""><br class=""></div><div><br class=""><blockquote type="cite" class=""><div class="">On Jan 14, 2021, at 12:08 PM, Oleg Grenrus <<a href="mailto:oleg.grenrus@iki.fi" class="">oleg.grenrus@iki.fi</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><span style="caret-color: rgb(0, 0, 0); font-family: Menlo-Regular; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">You need to define the type as a record.</span><br style="caret-color: rgb(0, 0, 0); font-family: Menlo-Regular; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><br style="caret-color: rgb(0, 0, 0); font-family: Menlo-Regular; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><span style="caret-color: rgb(0, 0, 0); font-family: Menlo-Regular; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">See</span><br style="caret-color: rgb(0, 0, 0); font-family: Menlo-Regular; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><a href="https://agda.readthedocs.io/en/v2.6.1/language/record-types.html#eta-expansion" style="font-family: Menlo-Regular; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;" class="">https://agda.readthedocs.io/en/v2.6.1/language/record-types.html#eta-expansion</a><br style="caret-color: rgb(0, 0, 0); font-family: Menlo-Regular; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><br style="caret-color: rgb(0, 0, 0); font-family: Menlo-Regular; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><span style="caret-color: rgb(0, 0, 0); font-family: Menlo-Regular; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">- Oleg</span><br style="caret-color: rgb(0, 0, 0); font-family: Menlo-Regular; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""></div></blockquote></div><br class=""></div></body></html>