idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-07 08:18:12 +03:00
Code Issues Projects Releases Wiki Activity

[ minor ] avoid repetition

Browse Source
This commit is contained in:
Guillaume ALLAIS 2020-12-07 18:04:04 +00:00 committed by G. Allais
parent f8c248dc7a
commit 39f26e7ed6
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/Compiler/RefC/RefC.idr
View File

@ -335,9 +335,10 @@ maxLineLengthForComment = 60
lJust : (line:String) -> (fillPos:Nat) -> (filler:Char) -> String
lJust line fillPos filler =
case isLTE (length line) fillPos of
let n = length line in
case isLTE n fillPos of
(Yes prf) =>
let missing = minus fillPos (length line)
let missing = minus fillPos n
fillBlock = pack (replicate missing filler)
in
line ++ fillBlock