List of tactics to develop:

[MatthewDaggitt]

• Presburger arithmetic (Add agda-presburger into stdlib #1041)
• Deriving Setoid, DecSetoid, PartialOrder etc. automatically for basic datatypes.

[MatthewDaggitt]

I have a student who has just contacted me who is specifically interested in look at the deriving tactics. @JacquesCarette would it be okay for them to take that on?

[JacquesCarette]

Sure!