mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-03 12:33:26 +03:00
Merge pull request #375 from edwinb/interactive
Add new clause at next blank line
This commit is contained in:
commit
fb9f79e3c6
@ -234,7 +234,11 @@ rtrim : String -> String
|
||||
rtrim str = reverse (ltrim (reverse str))
|
||||
|
||||
addClause : String -> Nat -> List String -> List String
|
||||
addClause c Z xs = rtrim c :: xs
|
||||
addClause c Z [] = rtrim c :: []
|
||||
addClause c Z (x :: xs)
|
||||
= if all isSpace (unpack x)
|
||||
then rtrim c :: x :: xs
|
||||
else x :: addClause c Z xs
|
||||
addClause c (S k) (x :: xs) = x :: addClause c k xs
|
||||
addClause c (S k) [] = [c]
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user