[Agda] Builtins

[Kirill Elagin]

As far as I know, it is only used for the `rewrite` syntax (and probably
`primTrustMe`, but I don’t know much about this last one, to be honest).

On Sat, Apr 25, 2015 at 11:50 AM N. Raghavendra <raghu at hri.res.in> wrote:

> I'm writing a homotopy type theory library for myself, which is
> independent of the Agda stdlib, and of the HoTT-Agda library available
> elsewhere.  I've defined equality as in Relation.Binary.Core of Agda
> stdlib.  Now, I am wondering whether to copy the pragmas
>
> {-# BUILTIN EQUALITY _≡_ #-}
> {-# BUILTIN REFL refl #-}
>
> to my file.  I don't understand what they mean.  What is the effect of
> these instructions?  Do they establish some kind of relation between
> judgemental equality, and the propositional equality that's defined in
> Relation.Binary.Core.  For instance, do they say that judgemental
> equality implies propositional equality?
>
> I gather from the ref. manual that BUILTIN pragmas tell Agda that the
> "given name implements one of the builtin types".  refl is only a
> constructor, not a type.  I'd really appreciate if someone explained all
> this.
>
> (I apologise if all this is trivial.  I come from another area of
> mathematics, and am not familiar with type theory and proof assistants.)
>
> Thanks and cheers,
> Raghu.
>
> --
> N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
> Harish-Chandra <http://www.retrotexts.net/Harish-Chandra> Research
> Institute, http://www.hri.res.in/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150425/3dd20704/attachment.html