edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-26 06:11:50 +03:00
Code Issues Projects Releases Wiki Activity

[ cosmetic ] various whitespace issues

Browse Source
This commit is contained in:
Guillaume Allais 2020-04-02 17:27:01 +01:00
parent d433eafa97
commit c5903c45e1
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
idris2.ipkg
View File

@ -1,6 +1,6 @@
package idris2 package idris2
modules = modules =
Compiler.Common, Compiler.Common,
Compiler.CompileExpr, Compiler.CompileExpr,
Compiler.Inline, Compiler.Inline,

2
libs/prelude/Prelude.idr
View File

@ -650,7 +650,7 @@ Ord Nat where
public export public export
natToInteger : Nat -> Integer natToInteger : Nat -> Integer
natToInteger Z = 0 natToInteger Z = 0
natToInteger (S k) = 1 + natToInteger k natToInteger (S k) = 1 + natToInteger k
-- integer (+) may be non-linear in second -- integer (+) may be non-linear in second
-- argument -- argument