add export of Pseudolattice.Property in Pseudolattice

LorenzoMolena · LorenzoMolena · commit 5b03cc32ea3d · 2025-12-14T01:39:25.000+01:00
diff --git a/Cubical/Relation/Binary/Order/Pseudolattice.agda b/Cubical/Relation/Binary/Order/Pseudolattice.agda
@@ -1,3 +1,4 @@
 module Cubical.Relation.Binary.Order.Pseudolattice where
 
 open import Cubical.Relation.Binary.Order.Pseudolattice.Base public
+open import Cubical.Relation.Binary.Order.Pseudolattice.Properties public

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
`1`	`1`	`module Cubical.Relation.Binary.Order.Pseudolattice where`
`2`	`2`
`3`	`3`	`open import Cubical.Relation.Binary.Order.Pseudolattice.Base public`
	`4`	`+open import Cubical.Relation.Binary.Order.Pseudolattice.Properties public`