Search the Lean import graph by module name to inspect its dependencies, reverse dependencies, and the part of the source tree affected by a change.
FloatLib supplies the generic scalar formats and numerical theory; NN.Floats contains
TorchLean’s adapters. External imports appear in the explorer, but their source trees are not
expanded here.
Import Graph
Each edge means that one Lean module directly imports another.
Loading import graph…
Source Snapshot
The site build reads these counts from the TorchLean checkout, including tests and guide sources. Dependency sources, including FloatLib, are excluded. Declaration headers measure source size; they do not measure proof coverage.
Loading source statistics…
Module Explorer
Click a module to see its direct imports and direct importers.
Matching Modules
Selected Module
Select a module on the left.