Text.ILex.Internal.Runner

Some utilities mainly for internal use

Definitions

offsetToIx : (o : Nat) -> Ix s (o + s)

Totality: total
Visibility: export

toBS : IBuffer n -> (from : Ix m n) -> (0 till : Nat) -> {auto ix : Ix till n} -> {auto 0 _ : LTE (ixToNat from) (ixToNat ix)} -> ByteString

Totality: total
Visibility: export

toBSP : ByteString -> IBuffer n -> (from : Ix m n) -> (0 till : Nat) -> {auto ix : Ix till n} -> {auto 0 _ : LTE (ixToNat from) (ixToNat ix)} -> ByteString

Totality: total
Visibility: export