fix(init/meta/expr.lean): is_app_of can return true for constants as well

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)

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)

tests/lean/dunfold_constant.lean

@@ -0,0 +1,2 @@
+def foo : list ℕ := [2]
+lemma bar : foo = foo := by dunfold foo

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'