There are two mechanisms for writing custom tactics in Idris: high and low level reflection.
Using high-level reflection, you write a function that runs in syntax and not on evaluated data — this will not reduce its argument. These functions return a new tactic, defined using pre-existing tactics in Idris. If you want to return evidence immediately, you can always use Exact . An example of such a reflection can be found in the effects library . Using byReflection in evidence mode calls up high-level reflection tactics.
In low-level reflection, you directly work with quoted terms from the theory of the Idris kernel type. Tactics is a function in TT -> List (TTName, TT) -> Tactic , where the first argument is the type of target, the second is the local context of the proof, and the return result is the same as with a high-level reflection. This is what is ridiculously related to the above . They are called using applyTactic in proof mode.