TorchLean API Reference

Start with one import NN

The complete TorchLean library.

Write model code NN.API

The focused application API for models, data, and training.

Work with tensors NN.Tensor

The focused tensor, shape, and operation import.

Inspect graph IR NN.IR.Graph

The op-tagged graph representation used by lowering and verification.

Read operator semantics NN.IR.Semantics

The executable meaning attached to IR operators and graph evaluation.

Run training code NN.Runtime

Runtime autograd, compiled execution, and training support.

Check certificates NN.Verification

The registered certificate and verification command surface.

Audit Float32 execution NN.Floats.IEEEExec

Executable IEEE-754 binary32 semantics used in float audits.

Browse By Layer

API Spec Runtime IR GraphSpec Proofs Verification Examples

Start from the thing you want to do, then jump into the declaration namespace from there.

Write model code NN.API Inspect lowering NN.IR.Graph Run autograd NN.Runtime Check certificates NN.Verification

The colored stripe on each declaration page marks what Lean generated.

def / instance theorem structure / class axiom / opaque