Merge pull request #3265 from andrevidela/fix-fixity-warning

fix error message for unexported fixities
idris-lang · Apr 21, 2024 · 517b283 · 517b283
2 parents 1dc7b74 + dd99186
commit 517b283
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr
@@ -1021,6 +1021,7 @@ mutual
   displayFixity : Maybe Visibility -> BindingModifier -> Fixity -> Nat -> OpStr -> String
   displayFixity Nothing NotBinding fix prec op = "\{show fix} \{show  prec} \{show op}"
   displayFixity Nothing bind fix prec op = "\{show bind} \{show fix} \{show  prec} \{show op}"
+  displayFixity (Just vis) NotBinding fix prec op = "\{show vis} \{show fix} \{show  prec} \{show op}"
   displayFixity (Just vis) bind fix prec op = "\{show vis} \{show bind} \{show fix} \{show  prec} \{show op}"
 
   -- Given a high level declaration, return a list of TTImp declarations

diff --git a/tests/idris2/operators/operators009/expected b/tests/idris2/operators/operators009/expected
@@ -1,8 +1,8 @@
 1/1: Building Test (Test.idr)
 Warning: Fixity declaration 'infixr 0 =@' does not have an export modifier, and
 will become private by default in a future version.
-To expose it outside of its module, write 'export regular infixr 0 =@'. If you
-intend to keep it private, write 'private regular infixr 0 =@'.
+To expose it outside of its module, write 'export infixr 0 =@'. If you
+intend to keep it private, write 'private infixr 0 =@'.
 
 Test:2:1--2:12
  1 |