[Agda] Re: Builtins

[N. Raghavendra]

At 2015-04-25T10:50:37Z, Kirill Elagin wrote:

> “Judgmental equality” is the computational one, that is, two terms
> are judgmentally equal iff they are equal up to reductions (which are
> built into Agda or any other type system), or, to be more precise,
> they are in the same equivalence class of the reflexive, symmetric,
> transitive closure of all the reduction rules. Basically, this means,
> they have the same normal form.

Many thanks for the clear explanation.  I have one more question about
judgemental equality.  Namely, suppose I have two terms a and b of the
same type A, and suppose that the following thing type-checks:

theorem : a ≡ b
theorem = refl

where ≡ are as in Relation.Binary.Core.  Does it mean then that a is
judgementally equal to b?

Cheers,
Raghu.

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