Inputs for Optional Batching

The input precedes the defaulted batch flag in training and loss functions. These instances give sample literals their expected type once the flag is selected, without coercing or copying data.

class TorchLean.Internal.BatchInput (single many : Type) (batch : Bool) (Input : outParam Type) : Prop

The selected batch flag determines the exact input type.

• type_eq : Input = if batch = true then many else single

  Input types must agree; batching never converts an arbitrary input.

instance TorchLean.Internal.instBatchInputFalse {single many : Type} : BatchInput single many false single

instance TorchLean.Internal.instBatchInputTrue {single many : Type} : BatchInput single many true many