What is a term of the type $\bot\rightarrow A$? The sentence $\bot\rightarrow A$ is provable in intuitionistic logic for any type $A$. The proof is trivial:

\begin{align}
\bot&amp;\vdash\bot \\
\hline
\bot&amp;\vdash A \\
\hline
&amp;\vdash\bot\rightarrow A
\end{align}
It means there has to be a lambda term with this type (the type has to be inhabited). What is it?
There are several ways of writing such a term, depending on how we write the proof terms for the elimination rule for $\bot$, which is
$$\frac{\quad\bot\quad}{A}$$
The corresponding rule in $\lambda$-calculus is
$$\frac{\Gamma \vdash e : \bot}{\Gamma \vdash \mathtt{absurd}_A(e) : A}.$$
(We call $\mathtt{absurd}_A$ an eliminator.)
Thus, the term of type $\bot \to A$ you seek is simply
$$\lambda x : \bot \,.\, \mathtt{absurd}_A(x).$$
Another way of writing the same thing is with a $\mathtt{match}$ statement. To see how this works, let us first consider a $\mathtt{match}$ statement for disjunctions. The elimination rule for $\lor$ is
$$\frac{A \lor B \qquad {\begin{matrix}A \\ \vdots \\ C\end{matrix}} \qquad {\begin{matrix}B \\ \vdots \\ C\end{matrix}}}{C}$$
The corresponding term constructor for $\lambda$-calculus can be written as
$$\frac{\Gamma \vdash e_1 : A+B \qquad \Gamma, x : A \vdash e_2 : C \qquad \Gamma, y : B \vdash e_3 : C}{\Gamma \vdash (\mathtt{match}\;e_1\;\mathtt{with}\;\mathtt{inl}(x) \to e_2 \mid \mathtt{inr}(y) \to e_3 \; \mathtt{end}) : C}$$
In general, the $\mathtt{match}$ statement which eliminates an $n$-fold sum $A_1 + A_2 + \cdots + A_n$ has $n$ cases.

The empty type $\bot$ is like a nullary sum, so it corresponds to a $\mathtt{match}$ statement with zero cases:
$$\frac{\Gamma \vdash e : \bot}{\Gamma \vdash (\mathtt{match}\;e\;\mathtt{with}\;\mathtt{end}) : C}$$
Indeed, this is how you can do it in Coq:

Definition ex_falso_quodlibet (A : Set) (x : Empty_set) : A :=
    match x with end.