We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 5da81d0 commit 31b51a6Copy full SHA for 31b51a6
src/Algebra/Apartness/Structures.agda
@@ -32,6 +32,7 @@ record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
32
33
open IsCommutativeRing isCommutativeRing public
34
open IsTightApartnessRelation isTightApartnessRelation public
35
+ using (isApartnessRelation; tight)
36
open IsApartnessRelation isApartnessRelation public
37
renaming
38
( irrefl to #-irrefl
0 commit comments