Skip to content

Commit c15f748

Browse files
committed
fix: deprecation via export of sym-≡
1 parent 08fb122 commit c15f748

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

src/Function/Properties/Bijection.agda

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -87,8 +87,9 @@ trans = Composition.bijection
8787

8888
-- Version 2.3
8989

90-
sym-≡ : Bijection S (setoid B) Bijection (setoid B) S
91-
sym-≡ = Symmetry.bijection-≡
90+
open Symmetry public
91+
using ()
92+
renaming (bijection-≡ to sym-≡)
9293
{-# WARNING_ON_USAGE sym-≡
9394
"Warning: sym-≡ was deprecated in v2.3.
9495
Please use sym instead. "

0 commit comments

Comments
 (0)