Added a function, 'last', that returns the last element in a finite set
commit34392c9b0ecd4451bfb0b5348426a0ffa6ffb1b3
authorDaniel Waterworth <Da.Waterworth@gmail.com>
dateSun 16 Dec 2012, 14:32 (14 years ago)
parentbf1c22e
lib/Prelude/Fin.idr+4
@@ -24,3 +24,7 @@ strengthen {n = S k} (fS i) with (strengthen i)
2424 strengthen (fS k) | Left x = Left (fS x)
2525 strengthen (fS k) | Right x = Right (fS x)
2626strengthen f = Left f
27+
28+last : Fin (S n)
29+last {n=O} = fO
30+last {n=S _} = fS last