Skip to content

Commit

Permalink
[ upstream ] Adapt to the changes in idris-lang/Idris2#3415
Browse files Browse the repository at this point in the history
  • Loading branch information
spcfox authored and buzden committed Dec 18, 2024
1 parent e2c4c53 commit 8055815
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/Language/LSP/CodeAction/Utils.idr
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,8 @@ printClause l i (WithClause _ lhsraw rig wvraw prf flags csraw) = do
pure (relit l ((pack (replicate i ' ')
++ show lhs
++ " with \{showCount rig}(" ++ show wval ++ ")"
++ maybe "" (\ nm => " proof " ++ show nm) prf
-- TODO: remove `the` after fix idris-lang/Idris2#3418
++ maybe "" (the (_ -> _) $ \(rg, nm) => " proof " ++ showCount rg ++ show nm) prf
++ "\n"))
++ showSep "\n" cs)
printClause l i (ImpossibleClause _ lhsraw) = do
Expand Down

0 comments on commit 8055815

Please sign in to comment.