<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="">Hello,</div><div class=""><br class=""></div><div class="">when I load the following module, </div><div class=""><br class=""></div><div class=""><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(237, 97, 27);" class=""><div style="margin: 0px; font-stretch: normal; line-height: normal; color: rgb(194, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">open</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">import</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Agda.Builtin.Bool</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; color: rgb(194, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">open</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">import</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Agda.Builtin.Nat</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; color: rgb(194, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">open</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">import</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Agda.Builtin.String</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">open</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">import</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #c200ff" class="">Function</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">using</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">case_of_</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; color: rgb(0, 0, 0); min-height: 21px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; color: rgb(69, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">StringOrInt</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class="">x </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Bool</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Set</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; color: rgb(69, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">StringOrInt</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> x </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">case</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> x </span><span style="font-variant-ligatures: no-common-ligatures" class="">of</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">λ</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">where</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; color: rgb(0, 0, 0);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">true</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">Nat</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; color: rgb(0, 0, 0);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">false</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">String</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; color: rgb(0, 0, 0); min-height: 21px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; color: rgb(69, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">getStringOrInt</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class="">x </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Bool</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">StringOrInt</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> x</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; color: rgb(69, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">getStringOrInt</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> x </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">case</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> x </span><span style="font-variant-ligatures: no-common-ligatures" class="">of</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">λ</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">where</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; color: rgb(0, 0, 0);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">true</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #c200ff" class="">94</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; color: rgb(180, 36, 25);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">false</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="text-decoration: underline ; font-variant-ligatures: no-common-ligatures" class="">"Ninety Four"</span></div><div class=""><span style="text-decoration: underline ; font-variant-ligatures: no-common-ligatures" class=""><br class=""></span></div></div></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; min-height: 21px;" class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; min-height: 21px;" class="">… I get this error message:</div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; min-height: 21px;" class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; min-height: 21px;" class=""><div style="font-family: Menlo; margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">String != Nat</span></div><div style="font-family: Menlo; margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">when checking that the expression "Ninety Four" has type Nat</span></div><div style="font-family: Menlo; margin: 0px; font-stretch: normal; line-height: normal;" class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class="">Do lambdas only return one data type (in this case, Nat)?</div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class="">Cheers,</div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class="">Philippe</div><div style="font-family: Menlo; margin: 0px; font-stretch: normal; line-height: normal;" class=""><br class=""></div><div style="font-family: Menlo; margin: 0px; font-stretch: normal; line-height: normal;" class=""><br class=""></div></div></body></html>