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)
• CLI helpers
• 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 via the top-level NN facade.

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 demos), 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 tutorials, 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.

def NN.API.CLI.takeFlagValueOnce (args : List String) (key : String) : Except String (Option String × List String)

Strip at most one occurrence of a --key flag from an argument list.

Accepted forms:

• --key value
• --key=value

def NN.API.CLI.takeFlagValueOnce.go (eqPrefix keyTok : String) : List String → Option String → List String → Except String (Option String × List String)

def NN.API.CLI.hasFlagValue (args : List String) (key : String) : Bool

Return true when args contains --key value or --key=value.

def NN.API.CLI.takeBoolFlagOnce (args : List String) (key : String) : Except String (Bool × List String)

Remove a no-value boolean flag once, returning whether it appeared.

partial def NN.API.CLI.takeBoolFlagOnce.go (keyTok : String) : List String → Bool → List String → Except String (Bool × List String)

def NN.API.CLI.dropDashDash (args : List String) : List String

Drop the leading -- separator commonly used with lean --run.

def NN.API.CLI.requireNoArgs (args : List String) : Except String Unit

Fail if there are any unconsumed CLI arguments.

def NN.API.CLI.takeNatFlagOnce (args : List String) (key : String) : Except String (Option ℕ × List String)

Like takeFlagValueOnce, but parse the value as a Nat.

def NN.API.CLI.parseFloatLit (s : String) : Option Float

Parse a JSON-style floating-point literal. Accepts the same decimal forms as Lean.Json.

def NN.API.CLI.takeFloatFlagOnce (args : List String) (key : String) : Except String (Option Float × List String)

Like takeFlagValueOnce, but parse the value as a Float.

def NN.API.CLI.takePathFlagOnce (args : List String) (key : String) : Except String (Option System.FilePath × List String)

Like takeFlagValueOnce, but return the value as a System.FilePath.

structure NN.API.CLI.EpochBatch : Type

Common training flags that appear across many demos: --epochs and --batch.

• epochs : ℕ

  Number of epochs to train for.

• batch : ℕ

  Batch size.

def NN.API.CLI.takeEpochBatch (args : List String) (defaultEpochs defaultBatch : ℕ) : Except String (EpochBatch × List String)

Parse optional --epochs and --batch flags.

Returns the parsed values (falling back to the provided defaults) and the remaining args.

def NN.API.CLI.takeStepsOrEpochs (args : List String) (default : ℕ) : Except String (ℕ × List String)

Parse a --steps flag, but also accept --epochs as a synonym.

This is a small ergonomics helper for tutorials that use a step-based loop, while still letting users pass --epochs out of habit from typical PyTorch training code.

If both --steps and --epochs are provided, this errors.

def NN.API.CLI.takeSeed (args : List String) (default : ℕ := 0) : Except String (ℕ × List String)

Parse an optional --seed flag (defaults to the provided value).

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.

@[implicit_reducible]

instance NN.API.instReprFloat32Config : Repr Float32Config

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

@[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 demos and small 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 human-readable 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 small demos that want to construct tensors from Float lists.