Documentation

NumLib.Init

NumLib Init #

This is the root initialisation file for NumLib. It is imported (transitively) by every file in the library, exactly as Mathlib.Init is imported by every Mathlib file.

Its job is to activate the default linter set and pull in the common tactic suite so that every downstream file starts from a uniform baseline.