Stream: new members
Topic: meta def syntax error
Ken Roe (Jul 18 2018 at 02:00):
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 (Jul 18 2018 at 02:03):
the name of the def is
Mario Carneiro (Jul 18 2018 at 02:04):
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 (Jul 18 2018 at 03:10):
Or restarting lean.
Last updated: May 18 2021 at 16:25 UTC