ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-19 04:57:24 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #4795 from clayrat/patch-18

Browse Source 
add a couple of Fin operations
This commit is contained in:
Niklas Larsson 2019-12-21 13:39:10 +01:00 committed by GitHub
commit d5e3013c5d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 9 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
libs/base/Data/Fin.idr
View File

@ -65,6 +65,11 @@ weakenN : (n : Nat) -> Fin m -> Fin (m + n)
weakenN n FZ = FZ
weakenN n (FS f) = FS (weakenN n f)
||| Weaken the bound on a Fin using an inequality proof
weakenLTE : LTE n m -> Fin n -> Fin m
weakenLTE (LTESucc p) FZ = FZ
weakenLTE (LTESucc p) (FS f) = FS $ weakenLTE p f
||| Attempt to tighten the bound on a Fin.
||| Return `Left` if the bound could not be tightened, or `Right` if it could.
strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
@ -101,6 +106,10 @@ implementation MinBound (Fin (S n)) where
implementation MaxBound (Fin (S n)) where
maxBound = last
||| Add two Fins
addFin : (x : Fin n) -> (y : Fin m) -> Fin (finToNat x + m)
addFin FZ y = y
addFin (FS x) y = FS $ addFin x y
-- Construct a Fin from an integer literal which must fit in the given Fin