You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.)
The text was updated successfully, but these errors were encountered:
Oops, sorry. I tried to take this feedback into account before submission, but I didn't quite appreciate the amount of whitespace sensitivity, so I misinterpreted you. I will add this now.
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: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:
(Also, the code in the paper is using single opening quotes instead of backticks around
andThen
, which is another problem.)The text was updated successfully, but these errors were encountered: