From df499a5b64471bbfbffac97ff4602c8e12b2dba4 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 5 Apr 2022 16:13:01 +0200 Subject: [PATCH] feat: early coercion from TSyntax to Syntax --- src/Init/Notation.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index c3a21c6e2b..b9c4282f5e 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -7,6 +7,7 @@ Notation for operators defined at Prelude.lean -/ prelude import Init.Prelude +import Init.Coe -- DSL for specifying parser precedences and priorities @@ -20,6 +21,11 @@ syntax:65 (name := subPrio) prio " - " prio:66 : prio end Lean.Parser.Syntax +namespace Lean +instance : Coe (TSyntax k) Syntax where + coe stx := stx.raw +end Lean + macro "max" : prec => `(1024) -- maximum precedence used in term parsers, in particular for terms in function position (`ident`, `paren`, ...) macro "arg" : prec => `(1023) -- precedence used for application arguments (`do`, `by`, ...) macro "lead" : prec => `(1022) -- precedence used for terms not supposed to be used as arguments (`let`, `have`, ...)