[Agda] Re: Builtins

[Nicolas Pouillard]

On 04/25/2015 12:50 PM, Kirill Elagin wrote:
> On Sat, Apr 25, 2015 at 1:19 PM N. Raghavendra <raghu at hri.res.in
> <mailto:raghu at hri.res.in>> wrote:
>
> I’m not really sure what will happen if you define `EQUALITY` to be
> something non-symmetric or non-transitive but I believe this should be fine.

Agda carefully checks that the equality builtin you give exactly corresponds to the propositional, namely it checks the type of EQUALITY and of REFL and only one constructor is allowed.

-- 
Best regards,
-- NP