CODEWITHSUNDEEP
agda
Kk Shinkai
Kk Shinkai

Reputation: 336

Where is _≡⟨_⟩_ Agda standard lib?

I read such a piece of code in plfa.

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)

but _≡⟨_⟩_ is not in PropositionalEquality

The module Eq.≡-Reasoning doesn't export the following: _≡⟨_⟩_
when scope checking the declaration
  open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)

I only find it in Function.Related and Relation.Binary.HeterogeneousEquality. What is happening?

Upvotes: 7

Views: 547

Answers (1)

gallais
gallais

Reputation: 12113

_≡⟨_⟩_ is a syntax notation for step-≡ as you can see in Relation.Binary.PropositionalEquality.Core.

So if you want to control what you are importing, you need to refer to step-≡ instead.

Upvotes: 5

Related Questions