idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 10:18:23 +03:00
Code Issues Projects Releases Wiki Activity

libs: mark Data.Nat.lteAddRight as public export

Browse Source
This commit is contained in:
Jakub Okoński 2021-01-17 17:21:40 +01:00 committed by G. Allais
parent 515453329a
commit 1376bdf3f2
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/base/Data/Nat.idr
View File

@ -115,7 +115,7 @@ lteTransitive : LTE n m -> LTE m p -> LTE n p
lteTransitive LTEZero y = LTEZero
lteTransitive (LTESucc x) (LTESucc y) = LTESucc (lteTransitive x y)
export
public export
lteAddRight : (n : Nat) -> LTE n (n + m)
lteAddRight Z = LTEZero
lteAddRight (S k) {m} = LTESucc (lteAddRight {m} k)