The problem

problem.idr

module LexerTest

import Text.Lexer
import Data.List

data TokenKind =Sharp

Show TokenKind where 
    show Sharp = "#"

revertTokens : List TokenKind -> String
revertTokens (hd::tl) = 
    (foldl (\acc => \cur => acc ++ (show cur)) (show hd) tl)
revertTokens [] = ""

token_map : TokenMap TokenKind
token_map = [(is '#' ,\n => Sharp)]

lexMd : String -> Either (Int, Int) (List (TokenData TokenKind))
lexMd str
  = case lex token_map str of
         (tokens, _, _, "") => Right tokens
         (_, line, column, _) => Left $ (line, column)

fixTkns : (List TokenKind -> String) 
          -> Either (Int, Int) (List (TokenData TokenKind))
          -> String

fixTkns fn res = 
    case res of 
        Left x => ""
        Right list => fn (map TokenData.tok list)

public export
simpleMd : String
simpleMd = "####"

simpleMdRes : String
simpleMdRes = (fixTkns revertTokens (lexMd simpleMd))

simpleLex : simpleMdRes = simpleMd 
simpleLex = Refl