mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-01 14:27:19 +03:00
7e67ba4f35
Now by marking a method as multiplicity 0, we can explicitly say that it's compile time only, so we can use it to compute types based on other erased things - see tests/idris2/interface008 for a small example. This fixes #8 - at least in that it allows the interface to be expressed properly now, although the multiplicity annotations mean that unfortunately it can't be compatible with Idris 1.
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
|
|
|