From fea65d99345d959ac58cf410b31fafaaa59ded64 Mon Sep 17 00:00:00 2001 From: Elias Aebi Date: Mon, 12 Sep 2022 11:17:50 +0200 Subject: [PATCH] doc: fix an example in the Macro Overview --- doc/macro_overview.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/macro_overview.md b/doc/macro_overview.md index ae7a8a6806..d55f5a6f19 100644 --- a/doc/macro_overview.md +++ b/doc/macro_overview.md @@ -352,12 +352,12 @@ example (p : Prop) (h : p) (f : p -> False) : 3 = 2 := by In the above example, we're still using the sugar Lean provides for creating quotations, as it feels more intuitive and saves us some work. It is possible to forego the sugar altogether: -``` +```lean syntax (name := myExfalsoParser) "myExfalso" : tactic @[macro myExfalsoParser] def implMyExfalso : Lean.Macro := - fun stx => Lean.mkNode `Lean.Parser.Tactic.apply - #[Lean.mkAtomFrom stx "apply", Lean.mkCIdentFrom stx ``False.elim] + fun stx => pure (Lean.mkNode `Lean.Parser.Tactic.apply + #[Lean.mkAtomFrom stx "apply", Lean.mkCIdentFrom stx ``False.elim]) example (p : Prop) (h : p) (f : p -> False) : 3 = 2 := by myExfalso