9-add-a-basic-type-checker

This merge request implements a basic type-checker for Proost.

Here's a short description of the implementation:

• add normal_form()and whnf(), which respectively allow you to get the normal form and weak-head normal form of a term.
• Implement an untyped conversion checker. It checks whether two given terms are convertible (read, definitionally equal).
• Implement a type-checker based on bidirectional type-checking : the checker checks the type of lambda-abstractions, and infers the types of every other term in a bidirectional manner (read, mutually recursive).

/!\ This merge request only implements type-checking of terms in an empty environment (as in, it doesn't make use of other definitions in the environment), though it won't be too hard to add the feature at a later date.

This merge requests needs an extensive review, as well as many more tests. I am planning on making more tests in my spare-time.

Closes #9 (closed)