<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 17 January 2015 at 12:52, Andrew Pitts <span dir="ltr"><<a href="mailto:Andrew.Pitts@cl.cam.ac.uk" target="_blank">Andrew.Pitts@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div id=":1jk" class="" style="overflow:hidden">Is there a description somewhere of all the existing primitives that<br>
the current version of Agda knows about?</div></blockquote></div><br><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">No a description but from Agda's source code, the Agda.TypeChecking.Primitive.primitiveFunctions function shows the actual primitives functions (see <a href="https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Primitive.hs#L550">https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Primitive.hs#L550</a> ).</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small"><span style="font-family:arial,sans-serif">-- </span><br></div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr">Andrés</div></div></div></div>
</div></div>