[Agda] Re: Builtins

[N. Raghavendra]

At 2015-04-25T09:11:41Z, Kirill Elagin wrote:

> 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).

Many thanks for the reply!

Yes, I'd seen the note that "The builtin equality is used for the new
rewrite construct and the primTrustMe primitive described below." in the
release notes.  Does it mean that if I don't use rewrite and
primTrustMe, I don't need to put the instructions

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

in my file?  Also, what's the relation between the "builtin equality"
and "judgemental equality"?

Cheers,
Raghu.

----------------------------------------------------------------------

> 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 Research Institute, http://www.hri.res.in/
>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/