Ala Agda.

Given

type t = A | B | C of int

We should be able to

let f : t -> int = function <tab>

to have generated the snippet template

let f : t -> int = function
  | A   -> __
  | B   -> __
  | C x -> __ x

where __ and x are fields that can be navigated with <tab>, and filled in by the user.

E.g., given

if x then
  exp1
else
  exp2

a single command should be able to swap the expressions in the branches and negate the conditional.

Write

let foo : t -> q = ...

And get an interactive prompt presenting a navigable tree of function chains from t to q.

I want proof search over defined functions, not over the implementations of the functions.