From bb5ce6d04be122e9c8d75532e31c303f289e118c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 18 Aug 2017 17:00:40 -0700 Subject: [PATCH] fix(library/init/meta/interactive_base): incorrect pattern MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit @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":[""],"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? --- library/init/meta/interactive_base.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/interactive_base.lean b/library/init/meta/interactive_base.lean index 98a19a7544..3f3ea538d0 100644 --- a/library/init/meta/interactive_base.lean +++ b/library/init/meta/interactive_base.lean @@ -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 []