git.iko.soy/Idris-dev
on master help sign in
Added a function, 'last', that returns the last element in a finite set
34392c9Daniel Waterworth
lib/Prelude/Fin.idr+4
compare with master
unifiedsplit
@@ -24,3 +24,7 @@ strengthen {n = S k} (fS i) with (strengthen i)
24 strengthen (fS k) | Left x = Left (fS x)
24 strengthen (fS k) | Left x = Left (fS x)
25 strengthen (fS k) | Right x = Right (fS x)
25 strengthen (fS k) | Right x = Right (fS x)
26strengthen f = Left f
26strengthen f = Left f
27+
28+last : Fin (S n)
29+last {n=O} = fO
30+last {n=S _} = fS last