<div dir="ltr">As long as you don't need the machine integers to compute at compile time, you can set up the bindings with the foreign function interface:<br><div><br></div><div>postulate<br></div><div>  Int : Set</div><div>  intPlus : Int -> Int -> Int<br></div><div><br></div><div>-- Agda 2.5.2</div><div>{-# COMPILED_TYPE Int Int #-}<br></div><div>{-# COMPILED intPlus (+) #-}</div><div><br></div><div>-- Agda > 2.5.2</div><div>{-# COMPILE GHC Int = type Int #-}</div><div>{-# COMPILE GHC intPlus = (+) #-}</div><div><br></div><div>If you need compile time computations you will either have to do a modest amount of hacking on the Agda implementation (mainly in Agda.TypeChecking.Monad.Builtin and Agda.TypeChecking.Rules.Builtin), or make do with the builtin natural numbers which map to Haskell bignums (Integer rather than Int).</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Mar 2, 2017 at 7:38 PM, stvienna wiener <span dir="ltr"><<a href="mailto:stvienna@gmail.com" target="_blank">stvienna@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><span style="font-size:11pt;font-family:arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">Hi,<br><br></span><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">I am programming a benchmark in Agda and would like to use machine integers. I would need bindings similar to Agda.Builtin.Float.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">I know there was some Agda library in the past regarding Naturals on <a href="http://github.com" target="_blank">github.com</a> (perhaps from Alan Jeffrey?).</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">Did anyone use machine integers in Agda and has code? Or at least the link to the old code on github.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">Thanks & cheers,</span></p><span style="font-size:11pt;font-family:arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">Stephan</span></div>
</blockquote></div><br></div>