meta def syntax error

Stream: new members

[Ken Roe]

I was trying out the example from the Lean meta programming paper. However their example gives a syntax error:

open tactic
open monad
open expr
open smt_tactic

meta def findd : expr → list expr → tactic expr
| e [] := failed
| e (h::hs) :=
    do t ← infer_type h,
    (unify e t >> return h) <|> find e hs.

The "return" statement gives the following error: (Ignore the line numbers, I've got other stuff in the file)

traversal.lean:88:18: error
invalid expression
traversal.lean:88:18: error
command expected

This is with Lean 3.4.1. How do I fix the error?

[Mario Carneiro]

the name of the def is findd?

[Mario Carneiro]

the command expected error is often fixed by scrolling down or setting the lean checking mode (on the status bar) to "check visible files" instead of "check visible lines"

[Reid Barton]

Or restarting lean.