@@ -0,0 +1,31 @@
1+module main
2+
3+%default total
4+
5+data CoNat
6+ = Co Nat
7+ | Infinity
8+
9+S : CoNat -> CoNat
10+S (Co n) = Co (S n)
11+S Infinity = Infinity
12+
13+Sn_notzero : main.S n = Co 0 -> _|_
14+Sn_notzero = believe_me
15+
16+S_Co_not_Inf : S (Co n) = Infinity -> _|_
17+S_Co_not_Inf = believe_me
18+
19+S_inj : (n : CoNat) -> (m : CoNat) -> S n = S m -> n = m
20+S_inj (Co n) (Co _) refl = refl
21+S_inj (Co n) Infinity p = FalseElim (S_Co_not_Inf p)
22+S_inj Infinity (Co m) p = FalseElim (S_Co_not_Inf (sym p))
23+S_inj Infinity Infinity refl = refl
24+
25+swap : {n : Nat} -> Vect A n -> Vect A n
26+swap Nil = Nil
27+swap (x :: Nil) = x :: Nil
28+swap (x :: y :: xs) = (y :: x :: (swap xs))
29+
30+main : IO ()
31+main = print (swap [1,2,3,4,5])