46 lines
2.1 KiB
Text
46 lines
2.1 KiB
Text
[Elab.definition.body] «term_+++_» : Lean.TrailingParserDescr :=
|
|
Lean.ParserDescr.trailingNode `«term_+++_» 1022 1
|
|
(Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+++") (Lean.ParserDescr.cat `term 1))
|
|
[Elab.definition.body] myMacro._@.ppNotationCode._hyg.21 : Lean.Macro :=
|
|
fun (x : Lean.Syntax) =>
|
|
let discr : Lean.Syntax := x;
|
|
if Lean.Syntax.isOfKind discr `«term_+++_» = true then
|
|
let discr_1 : Lean.Syntax := Lean.Syntax.getArg discr 0;
|
|
let discr_2 : Lean.Syntax := Lean.Syntax.getArg discr 1;
|
|
let discr : Lean.Syntax := Lean.Syntax.getArg discr 2;
|
|
let rhs : Lean.Syntax := discr;
|
|
let lhs : Lean.Syntax := discr_1;
|
|
do
|
|
let info ← Lean.MonadRef.mkInfoFromRefPos
|
|
let scp ← Lean.getCurrMacroScope
|
|
let mainModule ← Lean.getMainModule
|
|
pure
|
|
(Lean.Syntax.node `Lean.Parser.Term.app
|
|
#[Lean.Syntax.ident info (String.toSubstring "Nat.add") (Lean.addMacroScope mainModule `Nat.add scp)
|
|
[(`Nat.add, [])],
|
|
Lean.Syntax.node `null #[lhs, rhs]])
|
|
else
|
|
let discr : Lean.Syntax := x;
|
|
throw Lean.Macro.Exception.unsupportedSyntax
|
|
[Elab.definition.body] unexpand._@.ppNotationCode._hyg.4 : Lean.PrettyPrinter.Unexpander :=
|
|
fun (x : Lean.Syntax) =>
|
|
let discr : Lean.Syntax := x;
|
|
if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then
|
|
let discr_1 : Lean.Syntax := Lean.Syntax.getArg discr 0;
|
|
let discr_2 : Lean.Syntax := Lean.Syntax.getArg discr 1;
|
|
if Lean.Syntax.matchesNull discr_2 2 = true then
|
|
let discr : Lean.Syntax := Lean.Syntax.getArg discr_2 0;
|
|
let discr_3 : Lean.Syntax := Lean.Syntax.getArg discr_2 1;
|
|
let rhs : Lean.Syntax := discr_3;
|
|
let lhs : Lean.Syntax := discr;
|
|
do
|
|
let info ← Lean.MonadRef.mkInfoFromRefPos
|
|
Lean.getCurrMacroScope
|
|
Lean.getMainModule
|
|
pure (Lean.Syntax.node `«term_+++_» #[lhs, Lean.Syntax.atom info "+++", rhs])
|
|
else
|
|
let discr : Lean.Syntax := Lean.Syntax.getArg discr 1;
|
|
throw Unit.unit
|
|
else
|
|
let discr : Lean.Syntax := x;
|
|
throw Unit.unit
|