agda/agda2hs

New `≡⟨_⟨` syntax for `≡˘⟨_⟩`?

Opened this issue · 0 comments

In the Agda standard library, the syntax of ≡˘⟨_⟩ was changed to ≡⟨_⟨. Maybe it should be changed here as well but I am not sure:

syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z