Skip to content

README.md

Latest commit

 

History

History
29 lines (19 loc) · 642 Bytes

README.md

File metadata and controls

29 lines (19 loc) · 642 Bytes
Raw

CompPoly tests

This directory contains Lean test modules for regression and behavioral checks.

Structure

Tests mostly mirror the CompPoly/ hierarchy under the CompPolyTests namespace. For example:

  • library module: CompPoly/Univariate/Raw.lean
  • test module: tests/CompPolyTests/Univariate/Raw.lean

Some tests are cross-cutting rather than one-to-one mirrors, and some mirror a whole subtree rather than a single module (for example, tests/CompPolyTests/Fields/Binary/BF128Ghash/).

Running tests

Build all tests:

lake test

Build a single test module:

lake build CompPolyTests.Univariate.Raw