git.iko.soy/Idris-dev
on da672ec help sign in
Idris-dev/test/error005/error005.idr
27 lines 337 B history raw
1module error005
3import Data.Fin
5-- Test the Prelude's error rewrites for Fin
7one : Fin 2
8one = 1
10two : Fin 2
11two = 2
13hahaha : (n : Nat) -> Fin n
14hahaha n = 0
16ok : (n : Nat) -> Fin (plus 2 n)
17ok n = 1
19notOk : (n : Nat) -> Fin (plus 2 n)
20notOk n = 2
22b0rken : Integer -> Fin 3
23b0rken n = fromInteger n
25x : Fin 4
26x = the (Fin 4) 5