Idris2Doc : Huffman.WayStep

Huffman.WayStep

(source)

Definitions

dataPin : Type
Totality: total
Visibility: public export
Constructors:
EndOfString : Pin
Forward : Fin256->Pin
GoBack : Fin256->Bits8->Pin
GoBack2 : Fin256->Bits8->Bits8->Pin

Hint: 
ShowPin
dataWayStep : Type
Totality: total
Visibility: public export
Constructor: 
MkWayStep : MaybeNat->Vect256Pin->WayStep

Hint: 
ShowWayStep
way256 : IArray256WayStep
Visibility: export