decl_noncomputable_reason

Stream: metaprogramming / tactics

[Eric Wieser]

What's going on here with docs#environment.decl_noncomputable_reason (new in the latest lean)? It seems to work from within run_cmd, but fail from within eval.

open tactic

def foo : ℕ := 1

-- 'failed'
#eval do
  e ← get_env,
  f ← e.decl_noncomputable_reason `foo,
  trace f

-- ok
run_cmd do
  e ← get_env,
  trace $ e.decl_noncomputable_reason `foo


noncomputable def bar : ℕ := classical.choice sorry

-- ok
#eval do
  e ← get_env,
  f ← e.decl_noncomputable_reason `bar,
  trace f

-- ok
run_cmd do
  e ← get_env,
  trace $ e.decl_noncomputable_reason `bar

[Eric Wieser]

Oh, this is nothing to do with the definition and everything to do with ←

[Eric Wieser]

I was not aware of docs#tactic.opt_to_tac

[Notification Bot]

This topic was moved here from #general > decl_noncomputable_reason by Eric Wieser