Scalar array inputs

Parsers over the elements of the arrays of lean4-scalar-arrays: HasPos instances for their slice iterators, and a runner named after each array type, such as parseUInt8Array for UInt8Array. A runner also takes a slice of the array; an array coerces to a slice of all its elements. Positions are indices in the underlying array, not in the slice. Parser.parseSlice remains the runner for String.Slice.

These arrays are named UInt8Array and Float64Array because core has ByteArray and FloatArray. parseFloatArray uses the same iterator as parseFloat64Array, so a parser for one runs on the other. parseByteArray uses ByteIterator instead, so only a parser that is polymorphic in the iterator runs on both it and parseUInt8Array.

@[instance_reducible]

instance ParseIt.instHasPosSliceIteratorUInt8 : HasPos ScalarArray.UInt8Array.SliceIterator UInt8

Positions are indices in the underlying array.

Equations

• ParseIt.instHasPosSliceIteratorUInt8 = { Pos := Nat, pos := fun (it : Std.Iter UInt8) => it.toUInt8Slice.start }

@[instance_reducible]

instance ParseIt.instHasPosSliceIteratorUInt16 : HasPos ScalarArray.UInt16Array.SliceIterator UInt16

Positions are indices in the underlying array.

Equations

• ParseIt.instHasPosSliceIteratorUInt16 = { Pos := Nat, pos := fun (it : Std.Iter UInt16) => it.toUInt16Slice.start }

@[instance_reducible]

instance ParseIt.instHasPosSliceIteratorUInt32 : HasPos ScalarArray.UInt32Array.SliceIterator UInt32

Positions are indices in the underlying array.

Equations

• ParseIt.instHasPosSliceIteratorUInt32 = { Pos := Nat, pos := fun (it : Std.Iter UInt32) => it.toUInt32Slice.start }

@[instance_reducible]

instance ParseIt.instHasPosSliceIteratorUInt64 : HasPos ScalarArray.UInt64Array.SliceIterator UInt64

Positions are indices in the underlying array.

Equations

• ParseIt.instHasPosSliceIteratorUInt64 = { Pos := Nat, pos := fun (it : Std.Iter UInt64) => it.toUInt64Slice.start }

@[instance_reducible]

instance ParseIt.instHasPosSliceIteratorUSize : HasPos ScalarArray.USizeArray.SliceIterator USize

Positions are indices in the underlying array.

Equations

• ParseIt.instHasPosSliceIteratorUSize = { Pos := Nat, pos := fun (it : Std.Iter USize) => it.toUSizeSlice.start }

@[instance_reducible]

instance ParseIt.instHasPosSliceIteratorInt8 : HasPos ScalarArray.Int8Array.SliceIterator Int8

Positions are indices in the underlying array.

Equations

• ParseIt.instHasPosSliceIteratorInt8 = { Pos := Nat, pos := fun (it : Std.Iter Int8) => it.toInt8Slice.start }

@[instance_reducible]

instance ParseIt.instHasPosSliceIteratorInt16 : HasPos ScalarArray.Int16Array.SliceIterator Int16

Positions are indices in the underlying array.

Equations

• ParseIt.instHasPosSliceIteratorInt16 = { Pos := Nat, pos := fun (it : Std.Iter Int16) => it.toInt16Slice.start }

@[instance_reducible]

instance ParseIt.instHasPosSliceIteratorInt32 : HasPos ScalarArray.Int32Array.SliceIterator Int32

Positions are indices in the underlying array.

Equations

• ParseIt.instHasPosSliceIteratorInt32 = { Pos := Nat, pos := fun (it : Std.Iter Int32) => it.toInt32Slice.start }

@[instance_reducible]

instance ParseIt.instHasPosSliceIteratorInt64 : HasPos ScalarArray.Int64Array.SliceIterator Int64

Positions are indices in the underlying array.

Equations

• ParseIt.instHasPosSliceIteratorInt64 = { Pos := Nat, pos := fun (it : Std.Iter Int64) => it.toInt64Slice.start }

@[instance_reducible]

instance ParseIt.instHasPosSliceIteratorISize : HasPos ScalarArray.ISizeArray.SliceIterator ISize

Positions are indices in the underlying array.

Equations

• ParseIt.instHasPosSliceIteratorISize = { Pos := Nat, pos := fun (it : Std.Iter ISize) => it.toISizeSlice.start }

@[instance_reducible]

instance ParseIt.instHasPosSliceIteratorFloat32 : HasPos ScalarArray.Float32Array.SliceIterator Float32

Positions are indices in the underlying array.

Equations

• ParseIt.instHasPosSliceIteratorFloat32 = { Pos := Nat, pos := fun (it : Std.Iter Float32) => it.toFloat32Slice.start }

@[instance_reducible]

instance ParseIt.instHasPosSliceIteratorFloat : HasPos ScalarArray.Float64Array.SliceIterator Float

Positions are indices in the underlying array.

Equations

• ParseIt.instHasPosSliceIteratorFloat = { Pos := Nat, pos := fun (it : Std.Iter Float) => it.toFloatSlice.start }

@[inline]

def ParseIt.Parser.parseUInt8Array {ε α : Type} (p : Parser ε ScalarArray.UInt8Array.SliceIterator UInt8 α) (s : ScalarArray.UInt8Array.Slice) : Except ε α

Run p on the elements of s, an array or a slice of one. Positions are indices in the array.

Equations

• p.parseUInt8Array s = p.parse (Std.Slice.iter s)

@[inline]

def ParseIt.Parser.parseUInt16Array {ε α : Type} (p : Parser ε ScalarArray.UInt16Array.SliceIterator UInt16 α) (s : ScalarArray.UInt16Array.Slice) : Except ε α

Run p on the elements of s, an array or a slice of one. Positions are indices in the array.

Equations

• p.parseUInt16Array s = p.parse (Std.Slice.iter s)

@[inline]

def ParseIt.Parser.parseUInt32Array {ε α : Type} (p : Parser ε ScalarArray.UInt32Array.SliceIterator UInt32 α) (s : ScalarArray.UInt32Array.Slice) : Except ε α

Run p on the elements of s, an array or a slice of one. Positions are indices in the array.

Equations

• p.parseUInt32Array s = p.parse (Std.Slice.iter s)

@[inline]

def ParseIt.Parser.parseUInt64Array {ε α : Type} (p : Parser ε ScalarArray.UInt64Array.SliceIterator UInt64 α) (s : ScalarArray.UInt64Array.Slice) : Except ε α

Run p on the elements of s, an array or a slice of one. Positions are indices in the array.

Equations

• p.parseUInt64Array s = p.parse (Std.Slice.iter s)

@[inline]

def ParseIt.Parser.parseUSizeArray {ε α : Type} (p : Parser ε ScalarArray.USizeArray.SliceIterator USize α) (s : ScalarArray.USizeArray.Slice) : Except ε α

Run p on the elements of s, an array or a slice of one. Positions are indices in the array.

Equations

• p.parseUSizeArray s = p.parse (Std.Slice.iter s)

@[inline]

def ParseIt.Parser.parseInt8Array {ε α : Type} (p : Parser ε ScalarArray.Int8Array.SliceIterator Int8 α) (s : ScalarArray.Int8Array.Slice) : Except ε α

Run p on the elements of s, an array or a slice of one. Positions are indices in the array.

Equations

• p.parseInt8Array s = p.parse (Std.Slice.iter s)

@[inline]

def ParseIt.Parser.parseInt16Array {ε α : Type} (p : Parser ε ScalarArray.Int16Array.SliceIterator Int16 α) (s : ScalarArray.Int16Array.Slice) : Except ε α

Run p on the elements of s, an array or a slice of one. Positions are indices in the array.

Equations

• p.parseInt16Array s = p.parse (Std.Slice.iter s)

@[inline]

def ParseIt.Parser.parseInt32Array {ε α : Type} (p : Parser ε ScalarArray.Int32Array.SliceIterator Int32 α) (s : ScalarArray.Int32Array.Slice) : Except ε α

Run p on the elements of s, an array or a slice of one. Positions are indices in the array.

Equations

• p.parseInt32Array s = p.parse (Std.Slice.iter s)

@[inline]

def ParseIt.Parser.parseInt64Array {ε α : Type} (p : Parser ε ScalarArray.Int64Array.SliceIterator Int64 α) (s : ScalarArray.Int64Array.Slice) : Except ε α

Run p on the elements of s, an array or a slice of one. Positions are indices in the array.

Equations

• p.parseInt64Array s = p.parse (Std.Slice.iter s)

@[inline]

def ParseIt.Parser.parseISizeArray {ε α : Type} (p : Parser ε ScalarArray.ISizeArray.SliceIterator ISize α) (s : ScalarArray.ISizeArray.Slice) : Except ε α

Run p on the elements of s, an array or a slice of one. Positions are indices in the array.

Equations

• p.parseISizeArray s = p.parse (Std.Slice.iter s)

@[inline]

def ParseIt.Parser.parseFloat32Array {ε α : Type} (p : Parser ε ScalarArray.Float32Array.SliceIterator Float32 α) (s : ScalarArray.Float32Array.Slice) : Except ε α

Run p on the elements of s, an array or a slice of one. Positions are indices in the array.

Equations

• p.parseFloat32Array s = p.parse (Std.Slice.iter s)

@[inline]

def ParseIt.Parser.parseFloat64Array {ε α : Type} (p : Parser ε ScalarArray.Float64Array.SliceIterator Float α) (s : ScalarArray.Float64Array.Slice) : Except ε α

Run p on the elements of s, an array or a slice of one. Positions are indices in the array.

Equations

• p.parseFloat64Array s = p.parse (Std.Slice.iter s)

@[inline]

def ParseIt.Parser.parseFloatArray {ε α : Type} (p : Parser ε ScalarArray.Float64Array.SliceIterator Float α) (xs : FloatArray) : Except ε α

Run p on the elements of xs. Positions are array indices.

Equations

• p.parseFloatArray xs = p.parse xs.toFloat64Array.iter