mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-06 07:23:11 +03:00
a972778eab
They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
21 lines
347 B
Idris
21 lines
347 B
Idris
data Fin : Nat -> Type where
|
|
FZ : Fin (S k)
|
|
FS : Fin k -> Fin (S k)
|
|
|
|
interface Finite t where
|
|
0 card : Nat
|
|
to : t -> Fin card
|
|
|
|
implementation Finite (Fin k) where
|
|
card = k
|
|
to = id
|
|
|
|
interface BadFinite t where
|
|
badcard : Nat
|
|
badto : t -> Fin card
|
|
|
|
implementation BadFinite (Fin k) where
|
|
badcard = k
|
|
badto = id
|
|
|