Hoare

This is a WIP implementation of a basic Hoare Logic for a standard "While" imperative (toy) language.

We use Lean's notation extensions to display Hoare triples in the standard notation {P}c{Q}, using the concrete syntax of the "While" language.