[Agda] _≡⟨_⟩_ operator

Philippe de Rochambeau phiroc at free.fr
Mon May 4 18:27:58 CEST 2020


Hello,

The https://plfa.github.io/Induction Page mentions the _≡⟨_⟩_ operator, which I couldn’t find on https://agda.github.io/agda-stdlib/Relation.Binary.PropositionalEquality.Core.html

Does it have an existing equivalent in the Standard Library?

Cheers,

Philippe

PS My apologies if this question has already been asked on this list


More information about the Agda mailing list