[Agda] Strict equality _≣_ in agda

[Andreas Abel]

 > strict equality _≣_

Oh, I missed the fourth bar.  Why don't we also have "super-strict 
equality" with 5 stacked dashes?  :D

This must be the reason why the Chinese number system uses "number of 
dashes" only for the numerals 1, 2, and 3.  Thousands of years of wisdom...

On 2020-04-21 10:01, James Wood wrote:
> Hi Herminie,
> 
> I've seen this symbol be used in a similar way to how _≈_ is used in
> stdlib (a non-specific equivalence relation). It's probably fine to use
> for whatever you want, particularly if you can't use _≈_ due to a name
> clash.
> 
> Regards,
> James
> 
> On 21/04/2020 08:03, Herminie Pagel wrote:
>> Hi,
>>
>> Is there a standard interpretation of the strict equality _≣_ (latex
>> \===) in agda similar to the standard interpretation of _≡_  as the
>> identity type former?
>>
>> best,
>>
>> -- h
>>
>> _______________________________________________
>> 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
>