I’m relatively new to Coq. I’ve learnt that proof mode is not restricted to constructing proofs (terms whose type is a proposition), but can in fact construct any term. I like this a lot because I’m not yet familiar with all Gallina ways of doing things, and more familiar with tactics. So, instead of doing

Fixpoint even (n : nat) :=
match n with
| O => True
| S O => False
| S (S n') => even n'
end.

… I prefer to do

Fixpoint even (n : nat) : Prop.
Proof. (* well, "Proof" *)
destruct n as [|n'].
- exact True.
- destruct n' as [|n''].
* exact False.
* exact (even n'').
Defined.

My question is very simple. Is there a way to do this, but in the local context of a proof while in proof mode, not as a toplevel definition? This is one thing I naively tried:

Goal exists f : nat -> nat, True.
Proof.
Fail exists (fun (x : nat) => (_ : nat)).
(* Cannot infer this placeholder of type "nat" in environment: x : nat *)

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.

To add to what Karl has said (Equations is wonderful), you can also inject ltac:(...) into your Gallina terms when you aren’t clear what the term should be, but you know the tactic that would solve that hole for you.

You may also take into account how documentation making tools deal with the Definition foo:<type>. Proof. ... Defined. pattern.
For instance, coqdoc’s popular -g option (applied to your first example) just produces Definition even (n:nat): Prop without more information.