<div dir="ltr"><div dir="ltr"><div>agda-ocaml is an experimental OCaml backend that uses Stephen Dolan's malfunction package to target OCaml's internal flambda representation. It is an extension of previous work by <span style="font-weight:normal"><font size="2"><span class="gmail-p-name gmail-vcard-fullname gmail-d-block gmail-overflow-hidden">Frederik Hanghøj Iversen and Jan Mas Rovira.</span></font></span></div><div><span style="font-weight:normal"><font size="2"><span class="gmail-p-name gmail-vcard-fullname gmail-d-block gmail-overflow-hidden"><br></span></font></span></div><div><span style="font-weight:normal"><font size="2"><span class="gmail-p-name gmail-vcard-fullname gmail-d-block gmail-overflow-hidden">The main features of this version is that it supports pragmas. You can use OCaml from Agda or export agda code as an OCaml module.</span></font></span></div><div><span style="font-weight:normal"><font size="2"><span class="gmail-p-name gmail-vcard-fullname gmail-d-block gmail-overflow-hidden"><br></span></font></span></div><div><span style="font-weight:normal"><font size="2"><span class="gmail-p-name gmail-vcard-fullname gmail-d-block gmail-overflow-hidden">The internal representation of agda mimics the internal representation of OCaml, so that any OCaml data type or function is easily accessible from Agda and the opposite.<br></span></font></span></div><div><span style="font-weight:normal"><font size="2"><span class="gmail-p-name gmail-vcard-fullname gmail-d-block gmail-overflow-hidden"><br></span></font></span></div><div><span style="font-weight:normal"><font size="2"><span class="gmail-p-name gmail-vcard-fullname gmail-d-block gmail-overflow-hidden">If you are interested in testing it, I managed to write some documentation in its github repository as well as its current limitations.<br></span></font></span></div><div><span style="font-weight:normal"><font size="2"><span class="gmail-p-name gmail-vcard-fullname gmail-d-block gmail-overflow-hidden"><br></span></font></span></div><div><span style="font-weight:normal"><font size="2"><span class="gmail-p-name gmail-vcard-fullname gmail-d-block gmail-overflow-hidden"><a href="https://github.com/xekoukou/agda-ocaml">https://github.com/xekoukou/agda-ocaml</a><br></span></font></span></div></div></div>