[Agda] Univalence via Agda's primTrustMe?

[Andrés Sicard-Ramírez]

On 17 January 2015 at 12:52, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk> wrote:

> Is there a description somewhere of all the existing primitives that
> the current version of Agda knows about?
>

No a description but from Agda's source code, the
Agda.TypeChecking.Primitive.primitiveFunctions function shows the actual
primitives functions (see
https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Primitive.hs#L550
).

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150117/ae87a178/attachment.html