git.iko.soy/Idris-dev
on 49fffbc help sign in
Idris-dev/test/error005/error005.idr
20 lines 255 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