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

[minor] Make base/Data.Nat.divNatNZ compile-time reducible (#689)

Browse Source 
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
This commit is contained in:
Ohad Kammar 2020-09-22 09:53:05 +01:00 committed by GitHub
parent c4abdb4480
commit e77b9b4631
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -187,11 +187,13 @@ export partial
modNat : Nat -> Nat -> Nat
modNat left (S right) = modNatNZ left (S right) SIsNotZ
export partial
-- 'public' to allow type-level division
public export total
divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
divNatNZ left Z p = void (p Refl)
divNatNZ left (S right) _ = div' left left right
where
public export
div' : Nat -> Nat -> Nat -> Nat
div' Z centre right = Z
div' (S left) centre right =