[Agda] Strict equality _≣_ in agda

[James Wood]

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
>