This weekend I am trying to prove transitive closure can be computed in Idris. The way I represent it is that I have f:(a -> a -> Type), this forms a type that is inhabited when a statement is true. I can wrap this into another type that represents transitiveness. I can get (Transitive f x), from which I can make a set: (Set (Transitive f x)). This type describes a set containing all symbols reachable from 'x', through some way they relate 'f'.
Idris has some flaws that annoy when using it. Those issues become clear when trying to prove injectivity for certain sort or functions that have multiple variables. Also it's sometimes quite dumb, forgetting how values computed too early and other times is remembers that quite too well.
-- Henri Tuhola