From f952dbc78e5d41ac1a2fea05b3fe7bcde015790f Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Fri, 2 Dec 2016 19:47:51 -0800 Subject: [PATCH] fix(init/meta/expr.lean): is_app_of can return true for constants as well --- library/init/meta/comp_value_tactics.lean | 2 +- library/init/meta/expr.lean | 2 +- tests/lean/dunfold_constant.lean | 2 ++ tests/lean/dunfold_constant.lean.expected.out | 4 ++++ 4 files changed, 8 insertions(+), 2 deletions(-) create mode 100644 tests/lean/dunfold_constant.lean create mode 100644 tests/lean/dunfold_constant.lean.expected.out diff --git a/library/init/meta/comp_value_tactics.lean b/library/init/meta/comp_value_tactics.lean index 3abd339638..65019e3276 100644 --- a/library/init/meta/comp_value_tactics.lean +++ b/library/init/meta/comp_value_tactics.lean @@ -51,7 +51,7 @@ do t ← target, exact pr) <|> (do type ← whnf type, - guard (is_app_of type `fin), + guard (is_napp_of type `fin 1), (a, b) ← returnopt (is_ne t), pr ← returnopt (mk_fin_val_ne_proof a b), exact pr) diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index 95f3831a59..8231d3128c 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -149,7 +149,7 @@ meta def is_constant_of : expr → name → bool | e n := ff meta def is_app_of (e : expr) (n : name) : bool := -is_app e && is_constant_of (get_app_fn e) n +is_constant_of (get_app_fn e) n meta def is_napp_of (e : expr) (c : name) (n : nat) : bool := to_bool (is_app_of e c ∧ get_app_num_args e = n) diff --git a/tests/lean/dunfold_constant.lean b/tests/lean/dunfold_constant.lean new file mode 100644 index 0000000000..cb6c3ca0e5 --- /dev/null +++ b/tests/lean/dunfold_constant.lean @@ -0,0 +1,2 @@ +def foo : list ℕ := [2] +lemma bar : foo = foo := by dunfold foo diff --git a/tests/lean/dunfold_constant.lean.expected.out b/tests/lean/dunfold_constant.lean.expected.out new file mode 100644 index 0000000000..d0d412360d --- /dev/null +++ b/tests/lean/dunfold_constant.lean.expected.out @@ -0,0 +1,4 @@ +dunfold_constant.lean:2:28: error: tactic failed, there are unsolved goals +state: +⊢ [2] = [2] +dunfold_constant.lean:2:0: error: unknown declaration 'sorry'