API Core

Public convenience API core on top of TorchLean's spec + runtime entrypoints.

This module holds the small foundational surface used by the higher-level API modules:

• scalar-role separation (Semantics vs Runtime)
• the slim CLI helper module re-exported from NN.API.CLI
• dtype dispatch
• tensor constructor re-exports

Most end-user code should not import this file directly; it is re-exported through NN.API.Public and the top-level NN import.

PyTorch Mapping

DType here plays a role similar to torch.dtype selection in Python, but it also encodes a key TorchLean distinction:

• some scalar types are executable (you can #eval / run examples), and
• some scalar types are proof-only (e.g. ℝ or a noncomputable float model).

@[reducible, inline]

abbrev NN.API.Semantics.Scalar (α : Type) : Type

Public name for TorchLean's generic scalar semantics contract.

Read this as:

• "the model/loss is allowed to do its math over α"
• not "this backend is executable"

That second role belongs to API.Runtime.Scalar.

def NN.API.Semantics.relu {α : Type} [Zero α] [Max α] (x : α) : α

Host-side scalar ReLU for task definitions and synthetic targets.

class NN.API.Runtime.Scalar (α : Type) : Type

Runtime conversion from host Float constants into a TorchLean scalar type.

PyTorch analogy:

• in Python examples, users write float literals directly and tensors inherit a runtime dtype;
• in TorchLean, examples often start from host Float literals and inject them into the chosen runtime scalar backend with Runtime.ofFloat.

• ofFloat : Float → α

  Convert a host Float literal into this runtime scalar backend.

def NN.API.Runtime.ofFloat {α : Type} [Scalar α] (x : Float) : α

Generic host-float injection for TorchLean scalar backends.

@[implicit_reducible]

instance NN.API.Runtime.instScalarFloat : Scalar Float

Float is already the host literal type, so injection is identity.

@[implicit_reducible]

instance NN.API.Runtime.instScalarIEEE32Exec : Scalar TorchLean.Floats.IEEE754.IEEE32Exec

Inject host Float literals into the executable IEEE-754 binary32 backend.

@[implicit_reducible]

instance NN.API.Runtime.instScalarDualOfZero {α : Type} [Scalar α] [Zero α] : Scalar (Runtime.Autograd.TorchLean.Dual α)

Inject host literals into the dual-number backend used by the runtime autograd engine.

We interpret a literal as a primal value with zero tangent/adjoint component.

@[implicit_reducible]

instance NN.API.Runtime.instScalarComplexOfZero {α : Type} [Scalar α] [Zero α] : Scalar (TorchLean.Complex α)

Inject host literals into TorchLean's parametric complex scalar (imaginary part defaults to 0).

@[implicit_reducible, defaultInstance 100]

instance NN.API.Runtime.instOfScientificOfScalar {α : Type} [Scalar α] : OfScientific α

Allow numeric literals like 0.1 to elaborate to any TorchLean runtime scalar backend.

structure NN.API.Float32Config : Type

Configuration for the float32 dtype option.

We support both:

• proof-only float32 semantics (mode = .fp32, noncomputable), and
• executable IEEE-754 float32 semantics (mode = .ieee754Exec).

• mode : TorchLean.Floats.Float32Mode

  Which float32 semantics backend to use.

def NN.API.instReprFloat32Config.repr : Float32Config → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.instReprFloat32Config : Repr Float32Config

@[implicit_reducible]

instance NN.API.instDecidableEqFloat32Config : DecidableEq Float32Config

def NN.API.instDecidableEqFloat32Config.decEq (x✝ x✝¹ : Float32Config) : Decidable (x✝ = x✝¹)

inductive NN.API.DType : Type

Scalar type choice for runnable executables.

This is a runtime selection mechanism used by example programs; the core library itself is parametric in the scalar type α.

PyTorch Mapping

This corresponds loosely to choosing dtype= in PyTorch, but with additional "proof-only" variants:

• .float uses Lean's builtin Float (executable, but its IEEE-754 behavior is trusted),
• .float32 uses TorchLean's float32 model (either proof-only or executable),
• .complex uses TorchLean's parametric complex scalar over a float32 backend,
• .real uses ℝ (proof-only; not executable).

• float : DType
• float32 (cfg : Float32Config := { }) : DType
• complex (cfg : Float32Config) : DType
• real : DType

@[implicit_reducible]

instance NN.API.instReprDType : Repr DType

def NN.API.instReprDType.repr : DType → ℕ → Std.Format

def NN.API.instDecidableEqDType.decEq (x✝ x✝¹ : DType) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance NN.API.instDecidableEqDType : DecidableEq DType

def NN.API.DType.isExecutable : DType → Bool

Whether this dtype can be used in an executable (IO/#eval) context.

def NN.API.DType.log : DType → IO Unit

Log a short description of the chosen dtype to stdout.

def NN.API.DType.Internal.parseFloat32Mode (v : String) : Except String TorchLean.Floats.Float32Mode

Parse a float32 mode selector string into a Float32Mode.

def NN.API.DType.Internal.parseDTypeValue (v : String) : Except String DType

Parse a dtype selector string into a DType.

def NN.API.DType.parseAndStripWithDefault (args : List String) (default : DType) : Except String (DType × List String)

Parse and remove dtype flags from CLI arguments, using default when no dtype flags are provided.

This is the same parsing logic as parseAndStrip, but it lets higher-level runners choose a different default dtype depending on context (e.g. CUDA eager requires Float).

def NN.API.DType.parseAndStrip (args : List String) : Except String (DType × List String)

Parse and remove dtype flags from CLI arguments.

Supported flags:

• --dtype <value> or --dtype=<value>
• --float32-mode <mode> or --float32-mode=<mode>

The two flags are mutually exclusive.

def NN.API.DType.withRuntime (dt : DType) (k : {α : Type} → [Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → [Runtime.Scalar α] → IO Unit) : IO (Except String Unit)

Run k under the scalar type selected by dt.

If dt is proof-only, this returns an error rather than trying to execute noncomputable code.

def NN.API.DType.withExec (dt : DType) (k : {α : Type} → [Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → (Float → α) → IO Unit) : IO (Except String Unit)

Run k under the scalar type selected by dt, passing an explicit cast function Float → α.

This is a convenient shape for executables that construct tensors from Float lists.