This repository was archived by the owner on Jul 24, 2024. It is now read-only.
This repository was archived by the owner on Jul 24, 2024. It is now read-only.
docs: issue with tactic_writing.md #901
Description
I see this error:
don’t know how to synthesize placeholder
context:
a b c : ℤ,
hyp : a = b
⊢ Type ?
Code below extracted from the file tactic_writing.md is designed to reproduce the error. Other examples from the file work fine, or else have some narration explaining why they don't work.
open tactic.interactive («have»)
open tactic (get_local infer_type)
open interactive (parse)
open lean.parser (ident)
open lean.parser (tk)
open interactive (loc.ns)
open interactive.types (texpr location)
meta def mul_left (q : parse texpr) : parse location → tactic unit
| (loc.ns [some h]) := do
e ← tactic.i_to_expr q,
H ← get_local h,
`(%%l = %%r) ← infer_type H,
«have» h ``(%%e*%%l = %%e*%%r)
``(congr_arg (λ x, %%e*x) %%H),
tactic.clear H
| _ := tactic.fail "mul_left takes exactly one location"
-- it gives me an error, why?
example (a b c : ℤ) (hyp : a = b) : c*a = c*b :=
begin
mul_left c at hyp,
exact hyp
end