Skip to content

Latest commit

 

History

History
20 lines (16 loc) · 779 Bytes

Toy.rst

File metadata and controls

20 lines (16 loc) · 779 Bytes
Raw

A toy project for learning Low*

In tutorial/, a complete Low* project with Makefile, specs, spec tests, Low* implementation and C tests is provided for your enjoyment. The project is about writing a toy bignum implementation -- addition is already written and the rest is up for you to complete.

This is by far the most comprehensive example so far, and contains some exercises left as comments at the bottom of the various. There are numerous comments about what is the preferred style.

.. toctree::
   tutorial/specs/Spec.Bignum
   tutorial/specs/Spec.Test
   tutorial/code/Impl.Bignum.Lemmas
   tutorial/code/Impl.Bignum
   tutorial/code/Impl.Bignum.Intrinsics

Once the project has been built, check out the final C test in tests/.