Zulip Chat Archive

Stream: new members

Topic: meta def syntax error

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 18 2018 at 02:03):

the name of the def is findd?

view this post on Zulip Mario Carneiro (Jul 18 2018 at 02:04):

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"

view this post on Zulip Reid Barton (Jul 18 2018 at 03:10):

Or restarting lean.

Last updated: May 18 2021 at 16:25 UTC