# Wrapping up

Congratulations! You’ve reached the end of an introduction to basic F*.

You should have learned the following main concepts:

Basic functional programming

Using types to write precise specifications

Writing proofs as total functions

Defining and working with new inductive types

Lemmas and proofs by induction

Throughout, we saw how F*’s use of an SMT solver can reduce the overhead of producing proofs, and you should know enough now to be productive in small but non-trivial F* developments.

However, it would be wrong to conclude that SMT-backed proofs in F* are all plain sailing. And there’s a lot more to F* than SMT proofs—so read on through the rest of this book.

But, if you do plan to forge ahead with mainly SMT-backed proofs, you should keep the following in mind before attempting more challenging projects.

It’ll serve you well to learn a bit more about how an SMT solver works
and how F* interfaces with it—this is covered in a few upcoming
sections, including a section on classical proofs and in understanding how F* uses Z3. Additionally, if you’re interested in doing proofs about
arithmetic, particularly nonlinear arithmetic, before diving in, you
would do well to read more about the F* library `FStar.Math.Lemmas`

and F* arithmetic settings.