idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 02:23:44 +03:00
Code Issues Projects Releases Wiki Activity

[ doc ] Remove typo from Prelude.plus doc string and

Browse Source 
reformat doc string for `Prelude.minus`
This commit is contained in:
Marek L 2023-01-24 22:03:01 +00:00 committed by G. Allais
parent 4bedaac811
commit 7ec96cea7f
2 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libs/prelude/Prelude/Types.idr
View File

@ -43,14 +43,14 @@ integerToNat x
-- Define separately so we can spot the name when optimising Nats
||| Add two natural numbers.
||| @ x the number to case-split on
||| @ y the other numberpublic export
||| @ y the other number
public export
plus : (x : Nat) -> (y : Nat) -> Nat
plus Z y = y
plus (S k) y = S (plus k y)
||| Subtract natural numbers. If the second number is larger than the first,
||| return 0.
||| Subtract natural numbers.
||| If the second number is larger than the first, return 0.
public export
minus : (left : Nat) -> Nat -> Nat
minus Z right = Z

2
tests/idris2/docs001/expected
View File

@ -1,7 +1,7 @@
Main> Prelude.plus : Nat -> Nat -> Nat
Add two natural numbers.
@ x the number to case-split on
@ y the other numberpublic export
@ y the other number
Totality: total
Visibility: public export
Main> data Prelude.Nat : Type