This is a literate idris module

module  Encoding2

Here's a first paragraph

Here's some inline code too

Define Some Things

data  IntEncoding  =  VarInt  |  FixInt
data  Endian  =  BigEndian  |  LittleEndian

data  Config:  IntEncoding  ->  Endian  ->  Type
MkConfig  :  (0  a  :  IntEncoding)  ->  (0  b  :  Endian)  ->  Config  a  b

Add a paragraph here

How about a block quote

  1. and an
  2. Ordered list
  3. mayhaps

oh look another section

stringTest  :  String
stringTest  =  "a String goes here"

stringWithEsc  :  String
stringWithEsc  =  "How about a \\ and some \"quotes\" and some \{show 6}"

Some text before

Oh look a footnote:1

Note

note

Tip

tip

Warning

warning

This one has two paragraphs

interface  Encode  (0  config:  Config  _  _)  (b  :  Type)   where
    encode:  b  ->  List  Bits8

interface  Decode  t  where
    decode:  List  Bits8  ->  t

-- writeint: IntEncoding -> Int -> List Bits8
-- writeint FixInt a = 1 :: Nil
-- writeint VarInt a = 0 :: Nil

implementation  {a:  _}  ->  {b:  _}  ->  Encode  (MkConfig  a  b)  Int  where
    encode  {a}  self  =  handleendian  b  (writeint  a  self)  where
        writeint:  IntEncoding  ->  Int  ->  List  Bits8
        writeint  FixInt  v  =  1  ::  Nil
        writeint  VarInt  v  =  0  ::  Nil

        handleendian:  Endian  ->  List  Bits8  ->  List  Bits8
        handleendian  BigEndian  list  =  reverse  list
        handleendian  LittleEndian  list  =  list

test  :  Int  ->  List  Bits8
test  x  =  encode  {config  =  MkConfig  VarInt  LittleEndian}  x

And some text after

  1. hahaha↩︎