Skip to content

Commit

Permalink
fix(tactic/resolve_constant): parameters are no longer a problem
Browse files Browse the repository at this point in the history
  • Loading branch information
cipher1024 committed Sep 6, 2020
1 parent edf549e commit b9d03a1
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 2 deletions.
12 changes: 10 additions & 2 deletions library/init/meta/tactic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -896,8 +896,16 @@ meta def intron_with

/-- Returns n fully qualified if it refers to a constant, or else fails. -/
meta def resolve_constant (n : name) : tactic name :=
do (expr.const n _) ← resolve_name n,
pure n
-- do (expr.const n _) ← resolve_name n,
-- pure n

do e ← resolve_name n,
match e with
| expr.const n _ := pure n
| _ := do
e ← to_expr e tt ff,
pure $ e.get_app_fn.const_name
end

meta def to_expr_strict (q : pexpr) : tactic expr :=
to_expr q
Expand Down
10 changes: 10 additions & 0 deletions tests/lean/run/resolve_name_bug.lean
Original file line number Diff line number Diff line change
Expand Up @@ -25,3 +25,13 @@ by simp [f_lemma1, f_lemma2]

end bla
end foo

section param

parameters x y : ℤ

lemma my_ext (s s' : set ℤ) (h : x ∈ s ↔ y ∈ s') : true := trivial

run_cmd tactic.resolve_constant `my_ext

end param

0 comments on commit b9d03a1

Please sign in to comment.