JAR: Join-Accumulate Refine

16.6. Primitive Decoders🔗

🔗def
Jar.Codec.decodeArrayD {α : Type} (n : Nat) (f : Decoder α) :
  Decoder (Array α)
Jar.Codec.decodeArrayD {α : Type}
  (n : Nat) (f : Decoder α) :
  Decoder (Array α)

Decode a fixed-size array (no count prefix). Inverse of encodeArray.

🔗def
Jar.Codec.decodeFixedNatD (n : Nat) : Decoder Nat
Jar.Codec.decodeFixedNatD (n : Nat) :
  Decoder Nat

Decode a fixed-width LE natural of exactly n bytes.

🔗def
Jar.Codec.decodeNatD : Decoder Nat
Jar.Codec.decodeNatD : Decoder Nat

𝓔⁻¹ : Decode a variable-length natural. Inverse of encodeNat.

🔗def
Jar.Codec.decodeOptionD {α : Type} (f : Decoder α) : Decoder (Option α)
Jar.Codec.decodeOptionD {α : Type}
  (f : Decoder α) : Decoder (Option α)

Decode an optional value. Inverse of encodeOption.

🔗def
Jar.Codec.decodeLengthPrefixedD : Decoder ByteArray
Jar.Codec.decodeLengthPrefixedD :
  Decoder ByteArray

Decode a length-prefixed blob. Inverse of encodeLengthPrefixed.

🔗def
Jar.Codec.decodeBitsD (n : Nat) : Decoder (Array Bool)
Jar.Codec.decodeBitsD (n : Nat) :
  Decoder (Array Bool)

Decode n bits packed LSB-first. Inverse of encodeBits.

🔗def
Jar.Codec.decodeCountPrefixedArrayD {α : Type} (f : Decoder α) :
  Decoder (Array α)
Jar.Codec.decodeCountPrefixedArrayD
  {α : Type} (f : Decoder α) :
  Decoder (Array α)

Decode a count-prefixed array. Inverse of encodeCountPrefixedArray.

🔗def
Jar.Codec.decodeWorkResultD : Decoder Jar.WorkResult
Jar.Codec.decodeWorkResultD :
  Decoder Jar.WorkResult

Decode a WorkResult. Inverse of encodeWorkResult.

🔗def
Jar.Codec.decodeOctetSeqD (n : Nat) : Decoder (OctetSeq n)
Jar.Codec.decodeOctetSeqD (n : Nat) :
  Decoder (OctetSeq n)

Decode a fixed-size OctetSeq.

🔗def
Jar.Codec.decodeHashD : Decoder Hash
Jar.Codec.decodeHashD : Decoder Hash

Decode a Hash (32 bytes).