<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=""><div class=""><br class=""></div><div class="">Hello,</div><div class="">compiling the following code from the 2.6.1 Agda Documentation causes the below error message.</div><div class=""><br class=""></div><div class=""><pre class=""><i class=""><span class="kr">module</span> <span class="n">HelloWorld</span> <span class="kr">where</span>
<span class="kr">open</span> <span class="kr">import</span> <span class="n">Agda.Builtin.IO</span>
<span class="kr">open</span> <span class="kr">import</span> <span class="n">Agda.Builtin.Unit</span>
<span class="kr">open</span> <span class="kr">import</span> <span class="n">Agda.Builtin.String</span>
<span class="kr">postulate</span>
<span class="nf">putStrLn</span> <span class="ow">:</span> String <span class="ow">→</span> IO ⊤
<span class="cm">{-# FOREIGN GHC import qualified Data.Text.IO as Text #-}</span>
<span class="cm">{-# COMPILE GHC putStrLn = Text.putStrLn #-}</span>
<span class="nf">main</span> <span class="ow">:</span> IO ⊤
main <span class="ow">=</span> putStrLn <span class="s">"Hello, World!"</span></i></pre><div class=""><br class=""></div></div><div class=""><br class=""></div><div class=""><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><i class="">Compilation error:</i></span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; min-height: 21px;" class=""><i class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></i></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><i class="">MAlonzo/RTE.hs:9:1: error:</i></span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><i class=""> Could not find module ‘Numeric.IEEE’</i></span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><i class=""> Use -v (or `:set -v` in ghci) to see a list of the files searched for.</i></span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><i class=""> |</i></span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><i class="">9 | import Numeric.IEEE ( IEEE(identicalIEEE, nan) )</i></span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><i class=""> | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^</i></span></div></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><br class=""></span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class="">How do you fix it?</div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class="">Many thanks.</div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class="">Philippe</div><div class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><br class=""></span></div></body></html>