1411    hand. For example it is very hard to see a problem with @{text nub}

  1411    hand. For example it is very hard to see a problem with @{text nub}

  1412    vs @{text distinctBy} with only experimental data---one would still

  1412    vs @{text distinctBy} with only experimental data---one would still

  1413    see the correct result but find that simplification does not simplify in well-chosen, but not

  1413    see the correct result but find that simplification does not simplify in well-chosen, but not

  1414    obscure, examples. We found that from an implementation

  1414    obscure, examples. We found that from an implementation

  1415    point-of-view it is really important to have the formal proofs of

  1415    point-of-view it is really important to have the formal proofs of

  1417    healthy suspicion when experimental data is used to back up

  1419    healthy suspicion when experimental data is used to back up

  1418    efficiency claims. For example Sulzmann and Lu write about their

  1420    efficiency claims. For example Sulzmann and Lu write about their

  1419    equivalent of @{term blexer_simp} ``...we can incrementally compute

  1421    equivalent of @{term blexer_simp} ``...we can incrementally compute

  1420    bitcoded parse trees in linear time in the size of the input''

  1422    bitcoded parse trees in linear time in the size of the input''

  1421    \cite[Page 14]{Sulzmann2014}. 

  1423    \cite[Page 14]{Sulzmann2014}. 

  1422    Given the growth of the

  1424    Given the growth of the

  1423    derivatives in some cases even after aggressive simplification, this

  1425    derivatives in some cases even after aggressive simplification, this

  1424    is a hard to believe fact. A similar claim about a theoretical runtime

  1426    is a hard to believe fact. A similar claim about a theoretical runtime

  1425    of @{text "O(n\<^sup>2)"} is made for the Verbatim lexer, which calculates

  1427    of @{text "O(n\<^sup>2)"} is made for the Verbatim lexer, which calculates

  1426    tokens according to POSIX rules~\cite{verbatim}. For this it uses Brzozowski's

  1428    tokens according to POSIX rules~\cite{verbatim}. For this it uses Brzozowski's

  1428    They write: ``The results of our empirical tests [..] confirm that Verbatim has

  1430    They write: ``The results of our empirical tests [..] confirm that Verbatim has

  1429    @{text "O(n\<^sup>2)"} time complexity.'' \cite[Section~VII]{verbatim}.

  1431    @{text "O(n\<^sup>2)"} time complexity.'' \cite[Section~VII]{verbatim}.

  1430    While their correctness proof for Verbatim is formalised in Coq, the claim about

  1432    While their correctness proof for Verbatim is formalised in Coq, the claim about

  1431    the runtime complexity is only supported by some emperical evidence obtained

  1433    the runtime complexity is only supported by some emperical evidence obtained

  1432    by using the code extraction facilities of Coq.

  1434    by using the code extraction facilities of Coq.