In section 5.1.3, in the Idris definition of the mush tactic, there's a syntax error. The code in the paper is this:

mush : Elab ()
mush =
  do attack
    x <- gensym "x"
    intro x
    try intros
    induction (Var x) ‘andThen‘ auto
    solve

This code will not compile in Idris because of the wrong indentation. All lines of the do-notation must align with the first line in the do-notation. It should be:

mush : Elab ()
mush =
  do attack
     x <- gensym "x"
     intro x
     try intros
     induction (Var x) `andThen` auto
     solve

(Also, the code in the paper is using single opening quotes instead of backticks around andThen, which is another problem.)