Defining functions in proof mode

If you want to combine syntactic and interactive construction of functions, the standard advice I give these days is to use Equations (with _ for what you want to build with tactics), which is nowadays part of the Coq Platform. See a simple use example.

1 Like