fix(library/init/meta/interactive_base): incorrect pattern
@kha I'm trying to improve the equation compiler. I have added a
preprocessing step, and got the following wierd output when testing
tests/lean/interactive/info_goal.lean
```
> {"record":{"doc":"This tactic applies to any goal. It gives directly the exact proof\nterm of the goal. Let `T` be our goal, let `p` be a term of type `U` then\n`exact p` succeeds iff `T` and `U` are definitionally equal.","source":,"state":"⊢ ℕ → ℕ","tactic_params":["<error while executing interactive.param_desc: don't know how to pretty print lean.parser.pexpr 2>"],"text":"exact","type":"interactive.parse interactive.types.texpr → tactic unit"},"response":"ok","seq_num":4}
```
The problem seems to be the pattern
`(parser.pexpr)
which is sugar for
`(parser.pexpr std.prec.max)
and will not match `(pexpr 2)`
So, I fixed it by replacing the pattern with `(parser.pexpr %%v).
However, it is not clear to me why it was working before.
Any ideas?
This commit is contained in:
parent
c149286f44
commit
bb5ce6d04b
1 changed files with 1 additions and 1 deletions
|
|
@ -100,7 +100,7 @@ if f₁.empty then f₂ else if f₂.empty then f₁ else f₁ ++ [" "] ++ f₂
|
|||
private meta def parser_desc_aux : expr → tactic (list format)
|
||||
| `(ident) := return ["id"]
|
||||
| `(ident_) := return ["id"]
|
||||
| `(parser.pexpr) := return ["expr"]
|
||||
| `(parser.pexpr %%v) := return ["expr"]
|
||||
| `(tk %%c) := list.ret <$> to_fmt <$> eval_expr string c
|
||||
| `(cur_pos) := return []
|
||||
| `(pure ._) := return []
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue