Waterproof for Bewijzen in de Wiskunde

Abstract

Waterproof is a proof assistant developped at Eindhoven University of Technology. It is used to teach students at Analysis I, how to proof mathematical statements. Waterproof will be implemented at the Bachelors course "Bewijzen in de wiskunde" at UU. This thesis explains Type Theory, Rocq and Waterproof needed to understand the material produced for this course.