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, typed graph execution, and training support.

Check certificates NN.Verification

The registered certificate and verification command surface.

Use FloatLib formats NN.Floats

TorchLean adapters for FloatLib's configured binary formats and rounded-real models.

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