<div dir="ltr"><div>Chris has brought to my attention that my presentation of Simplicity at this year's Scale by the Bay has been available for a few weeks at <a href="https://www.youtube.com/watch?v=M4XnDrRIKx8" target="_blank">https://www.youtube.com/watch?v=M4XnDrRIKx8</a>.  In that video I give a worked example of a shallow embedding of Simplicity into Agda and proving the correctness of a multi-bit adder.</div><div><br></div><div>Simplicity isn't officially being developed in Agda, however Agda has some features that make it a nice language to use for presentation purposes.  I am attaching the Agda source files (before and after) that I used for the presentation so that you can follow along.<br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
</blockquote></div></div>