<html><head></head><body><div style="font-family: Verdana;font-size: 12.0px;"><div>Hi Andreas,</div>
<div> </div>
<div>I have visited http://learnyouanagda.liamoc.net/pages/introduction.html to learn about Agda programming. Subsequently I had downloaded GNU Emac and Haskell Compiler. But I failed to setup Agda despite following the instructions there at the URL. I have posted below the errors and exceptions WinGHCi is throwing up. </div>
<div> </div>
<div>
<div>Prelude> $ agda-mode setup</div>
<div><interactive>:9:1: error:<br/>
parse error on input ‘$’<br/>
Perhaps you intended to use TemplateHaskell<br/>
Prelude> <br/>
Prelude> :load "emacs.exe"<br/>
target ‘emacs.exe’ is not a module name or a source file<br/>
Prelude> $ cabal install Agda</div>
<div><interactive>:12:1: error:<br/>
parse error on input ‘$’<br/>
Perhaps you intended to use TemplateHaskell<br/>
Prelude> TemplateHaskell</div>
<div><interactive>:13:1: error:<br/>
Data constructor not in scope: TemplateHaskell<br/>
Prelude> </div>
<div> </div>
</div>
<div>
<div>Please tell me what I am doing wrong here. In addition to this I have a question. I had a chance to briefly look into your paper titled "Well-founded Recursion with Copatterns and Sized Types" What are the implications of programming both finite and infinite structures for our target decidable(halting) as well as long-running non-halting apps running on blockchain? Does this mean it(Agda?) can support both halting apps such as a financial contract with definite expiry/expiry/redemption/maturity date/timestamp and non-halting long-running apps such as an online Autonomous Voice Agent and an automated forex trading bot simultaneously? </div>
<div> </div>
<div>I thought we can't possibly achieve this in Turing machines/digital computers or networks. Only futuristic SupraTuring hypercomputers and hypercomputing networks would be able to achieve this apparently impossible feat. </div>
<div> </div>
<div>I look forward to hearing from you.</div>
<div> </div>
<div>Regards,</div>
<div>Ren </div>
<div> </div>
<div> </div>
<div> </div>
</div></div></body></html>