1
1
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-22 04:11:31 +03:00
Idris2-boot/tests/idris2/basic018/Fin.idr
Michael Morgan e6121e0935 Remove trailing whitespace from Idris sources.
This is the result of running the command:

$ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} +

I confirmed before running it that this would not affect any markdown
formatting in documentation comments.
2019-10-25 14:24:25 -07:00

35 lines
828 B
Idris

data Fin : Nat -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
natToFin Z (S j) = Just FZ
natToFin (S k) (S j)
= case natToFin k j of
Just k' => Just (FS k')
Nothing => Nothing
natToFin _ _ = Nothing
integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
integerToFin x Z = Nothing
integerToFin x n = if x >= 0 then natToFin (fromInteger x) n else Nothing
data IsJust : Maybe a -> Type where
ItIsJust : IsJust (Just x)
-- Testing that %allow_overloads lets this one through!
fromInteger : {k : Nat} ->
(n : Integer) ->
{auto prf : IsJust (integerToFin n k)} ->
Fin k
fromInteger {k} n {prf}
= case integerToFin n k of
Just val => val
foo : Fin 5
foo = 3
bar : Fin 5
bar = 8