Text.ILex.Internal.Runner

Some utilities mainly for internal use

Definitions

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

Totality: total
Visibility: export

writeBS : IBuffer n -> (from : Ix m n) -> (0 till : Nat) -> {auto ix : Ix till n} -> {auto 0 _ : LTE (ixToNat from) (ixToNat ix)} -> Ref q ByteString -> F1' q

Totality: total
Visibility: export

writeBSP : ByteString -> IBuffer n -> (from : Ix m n) -> (0 till : Nat) -> {auto ix : Ix till n} -> {auto 0 _ : LTE (ixToNat from) (ixToNat ix)} -> Ref q ByteString -> F1' q

Totality: total
Visibility: export