70b27fb2d3
See issue #1694. There is an orthogonal issue. `simp` (and consequently `unfold`) cannot be used to reduce projections (e.g., `has_add.add`). This issue has been previously raised by @Armael, but it was not addressed yet.
11 lines
234 B
Text
11 lines
234 B
Text
def f : nat → nat → nat
|
|
| 0 := λ x, x
|
|
| (n+1) := λ x, x + 1
|
|
|
|
meta def check_expr (p : pexpr) (t : expr) : tactic unit :=
|
|
do e ← tactic.to_expr p, guard (t = e)
|
|
|
|
example (n : nat): f (n+1) n = n + 1 :=
|
|
begin
|
|
unfold f
|
|
end
|