Equations
- Lean.Elab.Command.expandMixfix = (fun withAttrKindGlobal stx => withAttrKindGlobal stx fun stx => let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.mixfix = true then let discr_1 := Lean.Syntax.getArg discr 0; if Lean.Syntax.isOfKind discr_1 `Lean.Parser.Term.attrKind = true then let discr_2 := Lean.Syntax.getArg discr_1 0; if Lean.Syntax.matchesNull discr_2 0 = true then let discr_3 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_3 `Lean.Parser.Command.infixl = true then let discr_4 := Lean.Syntax.getArg discr_3 0; let discr_5 := Lean.Syntax.getArg discr 2; if Lean.Syntax.isOfKind discr_5 `Lean.Parser.precedence = true then let discr_6 := Lean.Syntax.getArg discr_5 0; let discr_7 := Lean.Syntax.getArg discr_5 1; let discr_8 := Lean.Syntax.getArg discr 3; let yes := fun x name => let discr_9 := Lean.Syntax.getArg discr 4; let yes := fun x prio => let discr_10 := Lean.Syntax.getArg discr 5; let discr_11 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; let f := discr; let op := discr_10; let prec := discr_7; do let a ← Lean.evalPrec prec let prec1 : Lean.Syntax := Lean.quote (a + 1) let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.notation #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrKind #[Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info "notation", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence #[Lean.Syntax.atom info ":", prec]], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match name with | some name => #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.namedName #[Lean.Syntax.atom info "(", Lean.Syntax.atom info "name", Lean.Syntax.atom info ":=", name, Lean.Syntax.atom info ")"]] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match prio with | some prio => #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.namedPrio #[Lean.Syntax.atom info "(", Lean.Syntax.atom info "priority", Lean.Syntax.atom info ":=", prio, Lean.Syntax.atom info ")"]] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.identPrec #[Lean.Syntax.ident info (String.toSubstring "lhs") (Lean.addMacroScope mainModule `lhs scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence #[Lean.Syntax.atom info ":", prec]]], op, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.identPrec #[Lean.Syntax.ident info (String.toSubstring "rhs") (Lean.addMacroScope mainModule `rhs scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence #[Lean.Syntax.atom info ":", prec1]]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[f, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "lhs") (Lean.addMacroScope mainModule `lhs scp) [], Lean.Syntax.ident info (String.toSubstring "rhs") (Lean.addMacroScope mainModule `rhs scp) []]]]); if Lean.Syntax.isNone discr_9 = true then yes () none else let discr_10 := discr_9; if Lean.Syntax.matchesNull discr_10 1 = true then let discr_11 := Lean.Syntax.getArg discr_10 0; if Lean.Syntax.isOfKind discr_11 `Lean.Parser.Command.namedPrio = true then let discr := Lean.Syntax.getArg discr_11 0; let discr := Lean.Syntax.getArg discr_11 1; let discr := Lean.Syntax.getArg discr_11 2; let discr := Lean.Syntax.getArg discr_11 3; let discr_12 := Lean.Syntax.getArg discr_11 4; let prio := discr; yes () (some prio) else let discr_12 := Lean.Syntax.getArg discr_10 0; let discr_13 := Lean.Syntax.getArg discr 4; let discr_14 := Lean.Syntax.getArg discr 5; let discr_15 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_11 := discr_9; let discr_12 := Lean.Syntax.getArg discr 4; let discr_13 := Lean.Syntax.getArg discr 5; let discr_14 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported; if Lean.Syntax.isNone discr_8 = true then yes () none else let discr_9 := discr_8; if Lean.Syntax.matchesNull discr_9 1 = true then let discr_10 := Lean.Syntax.getArg discr_9 0; if Lean.Syntax.isOfKind discr_10 `Lean.Parser.Command.namedName = true then let discr := Lean.Syntax.getArg discr_10 0; let discr := Lean.Syntax.getArg discr_10 1; let discr := Lean.Syntax.getArg discr_10 2; let discr := Lean.Syntax.getArg discr_10 3; let discr_11 := Lean.Syntax.getArg discr_10 4; let name := discr; yes () (some name) else let discr_11 := Lean.Syntax.getArg discr_9 0; let discr_12 := Lean.Syntax.getArg discr 3; let discr_13 := Lean.Syntax.getArg discr 4; let discr_14 := Lean.Syntax.getArg discr 5; let discr_15 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_10 := discr_8; let discr_11 := Lean.Syntax.getArg discr 3; let discr_12 := Lean.Syntax.getArg discr 4; let discr_13 := Lean.Syntax.getArg discr 5; let discr_14 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_6 := Lean.Syntax.getArg discr 2; let discr_7 := Lean.Syntax.getArg discr 3; let discr_8 := Lean.Syntax.getArg discr 4; let discr_9 := Lean.Syntax.getArg discr 5; let discr_10 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_4 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_4 `Lean.Parser.Command.infix = true then let discr_5 := Lean.Syntax.getArg discr_4 0; let discr_6 := Lean.Syntax.getArg discr 2; if Lean.Syntax.isOfKind discr_6 `Lean.Parser.precedence = true then let discr_7 := Lean.Syntax.getArg discr_6 0; let discr_8 := Lean.Syntax.getArg discr_6 1; let discr_9 := Lean.Syntax.getArg discr 3; let yes := fun x name => let discr_10 := Lean.Syntax.getArg discr 4; let yes := fun x prio => let discr_11 := Lean.Syntax.getArg discr 5; let discr_12 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; let f := discr; let op := discr_11; let prec := discr_8; do let a ← Lean.evalPrec prec let prec1 : Lean.Syntax := Lean.quote (a + 1) let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.notation #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrKind #[Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info "notation", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence #[Lean.Syntax.atom info ":", prec]], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match name with | some name => #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.namedName #[Lean.Syntax.atom info "(", Lean.Syntax.atom info "name", Lean.Syntax.atom info ":=", name, Lean.Syntax.atom info ")"]] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match prio with | some prio => #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.namedPrio #[Lean.Syntax.atom info "(", Lean.Syntax.atom info "priority", Lean.Syntax.atom info ":=", prio, Lean.Syntax.atom info ")"]] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.identPrec #[Lean.Syntax.ident info (String.toSubstring "lhs") (Lean.addMacroScope mainModule `lhs scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence #[Lean.Syntax.atom info ":", prec1]]], op, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.identPrec #[Lean.Syntax.ident info (String.toSubstring "rhs") (Lean.addMacroScope mainModule `rhs scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence #[Lean.Syntax.atom info ":", prec1]]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[f, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "lhs") (Lean.addMacroScope mainModule `lhs scp) [], Lean.Syntax.ident info (String.toSubstring "rhs") (Lean.addMacroScope mainModule `rhs scp) []]]]); if Lean.Syntax.isNone discr_10 = true then yes () none else let discr_11 := discr_10; if Lean.Syntax.matchesNull discr_11 1 = true then let discr_12 := Lean.Syntax.getArg discr_11 0; if Lean.Syntax.isOfKind discr_12 `Lean.Parser.Command.namedPrio = true then let discr := Lean.Syntax.getArg discr_12 0; let discr := Lean.Syntax.getArg discr_12 1; let discr := Lean.Syntax.getArg discr_12 2; let discr := Lean.Syntax.getArg discr_12 3; let discr_13 := Lean.Syntax.getArg discr_12 4; let prio := discr; yes () (some prio) else let discr_13 := Lean.Syntax.getArg discr_11 0; let discr_14 := Lean.Syntax.getArg discr 4; let discr_15 := Lean.Syntax.getArg discr 5; let discr_16 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_12 := discr_10; let discr_13 := Lean.Syntax.getArg discr 4; let discr_14 := Lean.Syntax.getArg discr 5; let discr_15 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported; if Lean.Syntax.isNone discr_9 = true then yes () none else let discr_10 := discr_9; if Lean.Syntax.matchesNull discr_10 1 = true then let discr_11 := Lean.Syntax.getArg discr_10 0; if Lean.Syntax.isOfKind discr_11 `Lean.Parser.Command.namedName = true then let discr := Lean.Syntax.getArg discr_11 0; let discr := Lean.Syntax.getArg discr_11 1; let discr := Lean.Syntax.getArg discr_11 2; let discr := Lean.Syntax.getArg discr_11 3; let discr_12 := Lean.Syntax.getArg discr_11 4; let name := discr; yes () (some name) else let discr_12 := Lean.Syntax.getArg discr_10 0; let discr_13 := Lean.Syntax.getArg discr 3; let discr_14 := Lean.Syntax.getArg discr 4; let discr_15 := Lean.Syntax.getArg discr 5; let discr_16 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_11 := discr_9; let discr_12 := Lean.Syntax.getArg discr 3; let discr_13 := Lean.Syntax.getArg discr 4; let discr_14 := Lean.Syntax.getArg discr 5; let discr_15 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_7 := Lean.Syntax.getArg discr 2; let discr_8 := Lean.Syntax.getArg discr 3; let discr_9 := Lean.Syntax.getArg discr 4; let discr_10 := Lean.Syntax.getArg discr 5; let discr_11 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_5 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_5 `Lean.Parser.Command.infixr = true then let discr_6 := Lean.Syntax.getArg discr_5 0; let discr_7 := Lean.Syntax.getArg discr 2; if Lean.Syntax.isOfKind discr_7 `Lean.Parser.precedence = true then let discr_8 := Lean.Syntax.getArg discr_7 0; let discr_9 := Lean.Syntax.getArg discr_7 1; let discr_10 := Lean.Syntax.getArg discr 3; let yes := fun x name => let discr_11 := Lean.Syntax.getArg discr 4; let yes := fun x prio => let discr_12 := Lean.Syntax.getArg discr 5; let discr_13 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; let f := discr; let op := discr_12; let prec := discr_9; do let a ← Lean.evalPrec prec let prec1 : Lean.Syntax := Lean.quote (a + 1) let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.notation #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrKind #[Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info "notation", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence #[Lean.Syntax.atom info ":", prec]], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match name with | some name => #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.namedName #[Lean.Syntax.atom info "(", Lean.Syntax.atom info "name", Lean.Syntax.atom info ":=", name, Lean.Syntax.atom info ")"]] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match prio with | some prio => #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.namedPrio #[Lean.Syntax.atom info "(", Lean.Syntax.atom info "priority", Lean.Syntax.atom info ":=", prio, Lean.Syntax.atom info ")"]] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.identPrec #[Lean.Syntax.ident info (String.toSubstring "lhs") (Lean.addMacroScope mainModule `lhs scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence #[Lean.Syntax.atom info ":", prec1]]], op, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.identPrec #[Lean.Syntax.ident info (String.toSubstring "rhs") (Lean.addMacroScope mainModule `rhs scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence #[Lean.Syntax.atom info ":", prec]]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[f, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "lhs") (Lean.addMacroScope mainModule `lhs scp) [], Lean.Syntax.ident info (String.toSubstring "rhs") (Lean.addMacroScope mainModule `rhs scp) []]]]); if Lean.Syntax.isNone discr_11 = true then yes () none else let discr_12 := discr_11; if Lean.Syntax.matchesNull discr_12 1 = true then let discr_13 := Lean.Syntax.getArg discr_12 0; if Lean.Syntax.isOfKind discr_13 `Lean.Parser.Command.namedPrio = true then let discr := Lean.Syntax.getArg discr_13 0; let discr := Lean.Syntax.getArg discr_13 1; let discr := Lean.Syntax.getArg discr_13 2; let discr := Lean.Syntax.getArg discr_13 3; let discr_14 := Lean.Syntax.getArg discr_13 4; let prio := discr; yes () (some prio) else let discr_14 := Lean.Syntax.getArg discr_12 0; let discr_15 := Lean.Syntax.getArg discr 4; let discr_16 := Lean.Syntax.getArg discr 5; let discr_17 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_13 := discr_11; let discr_14 := Lean.Syntax.getArg discr 4; let discr_15 := Lean.Syntax.getArg discr 5; let discr_16 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported; if Lean.Syntax.isNone discr_10 = true then yes () none else let discr_11 := discr_10; if Lean.Syntax.matchesNull discr_11 1 = true then let discr_12 := Lean.Syntax.getArg discr_11 0; if Lean.Syntax.isOfKind discr_12 `Lean.Parser.Command.namedName = true then let discr := Lean.Syntax.getArg discr_12 0; let discr := Lean.Syntax.getArg discr_12 1; let discr := Lean.Syntax.getArg discr_12 2; let discr := Lean.Syntax.getArg discr_12 3; let discr_13 := Lean.Syntax.getArg discr_12 4; let name := discr; yes () (some name) else let discr_13 := Lean.Syntax.getArg discr_11 0; let discr_14 := Lean.Syntax.getArg discr 3; let discr_15 := Lean.Syntax.getArg discr 4; let discr_16 := Lean.Syntax.getArg discr 5; let discr_17 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_12 := discr_10; let discr_13 := Lean.Syntax.getArg discr 3; let discr_14 := Lean.Syntax.getArg discr 4; let discr_15 := Lean.Syntax.getArg discr 5; let discr_16 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_8 := Lean.Syntax.getArg discr 2; let discr_9 := Lean.Syntax.getArg discr 3; let discr_10 := Lean.Syntax.getArg discr 4; let discr_11 := Lean.Syntax.getArg discr 5; let discr_12 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_6 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_6 `Lean.Parser.Command.prefix = true then let discr_7 := Lean.Syntax.getArg discr_6 0; let discr_8 := Lean.Syntax.getArg discr 2; if Lean.Syntax.isOfKind discr_8 `Lean.Parser.precedence = true then let discr_9 := Lean.Syntax.getArg discr_8 0; let discr_10 := Lean.Syntax.getArg discr_8 1; let discr_11 := Lean.Syntax.getArg discr 3; let yes := fun x name => let discr_12 := Lean.Syntax.getArg discr 4; let yes := fun x prio => let discr_13 := Lean.Syntax.getArg discr 5; let discr_14 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; let f := discr; let op := discr_13; let prec := discr_10; do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.notation #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrKind #[Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info "notation", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence #[Lean.Syntax.atom info ":", prec]], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match name with | some name => #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.namedName #[Lean.Syntax.atom info "(", Lean.Syntax.atom info "name", Lean.Syntax.atom info ":=", name, Lean.Syntax.atom info ")"]] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match prio with | some prio => #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.namedPrio #[Lean.Syntax.atom info "(", Lean.Syntax.atom info "priority", Lean.Syntax.atom info ":=", prio, Lean.Syntax.atom info ")"]] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null #[op, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.identPrec #[Lean.Syntax.ident info (String.toSubstring "arg") (Lean.addMacroScope mainModule `arg scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence #[Lean.Syntax.atom info ":", prec]]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[f, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "arg") (Lean.addMacroScope mainModule `arg scp) []]]]); if Lean.Syntax.isNone discr_12 = true then yes () none else let discr_13 := discr_12; if Lean.Syntax.matchesNull discr_13 1 = true then let discr_14 := Lean.Syntax.getArg discr_13 0; if Lean.Syntax.isOfKind discr_14 `Lean.Parser.Command.namedPrio = true then let discr := Lean.Syntax.getArg discr_14 0; let discr := Lean.Syntax.getArg discr_14 1; let discr := Lean.Syntax.getArg discr_14 2; let discr := Lean.Syntax.getArg discr_14 3; let discr_15 := Lean.Syntax.getArg discr_14 4; let prio := discr; yes () (some prio) else let discr_15 := Lean.Syntax.getArg discr_13 0; let discr_16 := Lean.Syntax.getArg discr 4; let discr_17 := Lean.Syntax.getArg discr 5; let discr_18 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_14 := discr_12; let discr_15 := Lean.Syntax.getArg discr 4; let discr_16 := Lean.Syntax.getArg discr 5; let discr_17 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported; if Lean.Syntax.isNone discr_11 = true then yes () none else let discr_12 := discr_11; if Lean.Syntax.matchesNull discr_12 1 = true then let discr_13 := Lean.Syntax.getArg discr_12 0; if Lean.Syntax.isOfKind discr_13 `Lean.Parser.Command.namedName = true then let discr := Lean.Syntax.getArg discr_13 0; let discr := Lean.Syntax.getArg discr_13 1; let discr := Lean.Syntax.getArg discr_13 2; let discr := Lean.Syntax.getArg discr_13 3; let discr_14 := Lean.Syntax.getArg discr_13 4; let name := discr; yes () (some name) else let discr_14 := Lean.Syntax.getArg discr_12 0; let discr_15 := Lean.Syntax.getArg discr 3; let discr_16 := Lean.Syntax.getArg discr 4; let discr_17 := Lean.Syntax.getArg discr 5; let discr_18 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_13 := discr_11; let discr_14 := Lean.Syntax.getArg discr 3; let discr_15 := Lean.Syntax.getArg discr 4; let discr_16 := Lean.Syntax.getArg discr 5; let discr_17 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_9 := Lean.Syntax.getArg discr 2; let discr_10 := Lean.Syntax.getArg discr 3; let discr_11 := Lean.Syntax.getArg discr 4; let discr_12 := Lean.Syntax.getArg discr 5; let discr_13 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_7 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_7 `Lean.Parser.Command.postfix = true then let discr_8 := Lean.Syntax.getArg discr_7 0; let discr_9 := Lean.Syntax.getArg discr 2; if Lean.Syntax.isOfKind discr_9 `Lean.Parser.precedence = true then let discr_10 := Lean.Syntax.getArg discr_9 0; let discr_11 := Lean.Syntax.getArg discr_9 1; let discr_12 := Lean.Syntax.getArg discr 3; let yes := fun x name => let discr_13 := Lean.Syntax.getArg discr 4; let yes := fun x prio => let discr_14 := Lean.Syntax.getArg discr 5; let discr_15 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; let f := discr; let op := discr_14; let prec := discr_11; do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.notation #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrKind #[Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info "notation", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence #[Lean.Syntax.atom info ":", prec]], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match name with | some name => #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.namedName #[Lean.Syntax.atom info "(", Lean.Syntax.atom info "name", Lean.Syntax.atom info ":=", name, Lean.Syntax.atom info ")"]] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match prio with | some prio => #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.namedPrio #[Lean.Syntax.atom info "(", Lean.Syntax.atom info "priority", Lean.Syntax.atom info ":=", prio, Lean.Syntax.atom info ")"]] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.identPrec #[Lean.Syntax.ident info (String.toSubstring "arg") (Lean.addMacroScope mainModule `arg scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence #[Lean.Syntax.atom info ":", prec]]], op], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[f, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "arg") (Lean.addMacroScope mainModule `arg scp) []]]]); if Lean.Syntax.isNone discr_13 = true then yes () none else let discr_14 := discr_13; if Lean.Syntax.matchesNull discr_14 1 = true then let discr_15 := Lean.Syntax.getArg discr_14 0; if Lean.Syntax.isOfKind discr_15 `Lean.Parser.Command.namedPrio = true then let discr := Lean.Syntax.getArg discr_15 0; let discr := Lean.Syntax.getArg discr_15 1; let discr := Lean.Syntax.getArg discr_15 2; let discr := Lean.Syntax.getArg discr_15 3; let discr_16 := Lean.Syntax.getArg discr_15 4; let prio := discr; yes () (some prio) else let discr_16 := Lean.Syntax.getArg discr_14 0; let discr_17 := Lean.Syntax.getArg discr 4; let discr_18 := Lean.Syntax.getArg discr 5; let discr_19 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_15 := discr_13; let discr_16 := Lean.Syntax.getArg discr 4; let discr_17 := Lean.Syntax.getArg discr 5; let discr_18 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported; if Lean.Syntax.isNone discr_12 = true then yes () none else let discr_13 := discr_12; if Lean.Syntax.matchesNull discr_13 1 = true then let discr_14 := Lean.Syntax.getArg discr_13 0; if Lean.Syntax.isOfKind discr_14 `Lean.Parser.Command.namedName = true then let discr := Lean.Syntax.getArg discr_14 0; let discr := Lean.Syntax.getArg discr_14 1; let discr := Lean.Syntax.getArg discr_14 2; let discr := Lean.Syntax.getArg discr_14 3; let discr_15 := Lean.Syntax.getArg discr_14 4; let name := discr; yes () (some name) else let discr_15 := Lean.Syntax.getArg discr_13 0; let discr_16 := Lean.Syntax.getArg discr 3; let discr_17 := Lean.Syntax.getArg discr 4; let discr_18 := Lean.Syntax.getArg discr 5; let discr_19 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_14 := discr_12; let discr_15 := Lean.Syntax.getArg discr 3; let discr_16 := Lean.Syntax.getArg discr 4; let discr_17 := Lean.Syntax.getArg discr 5; let discr_18 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_10 := Lean.Syntax.getArg discr 2; let discr_11 := Lean.Syntax.getArg discr 3; let discr_12 := Lean.Syntax.getArg discr 4; let discr_13 := Lean.Syntax.getArg discr 5; let discr_14 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_8 := Lean.Syntax.getArg discr 1; let discr_9 := Lean.Syntax.getArg discr 2; let discr_10 := Lean.Syntax.getArg discr 3; let discr_11 := Lean.Syntax.getArg discr 4; let discr_12 := Lean.Syntax.getArg discr 5; let discr_13 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_3 := Lean.Syntax.getArg discr_1 0; let discr_4 := Lean.Syntax.getArg discr 1; let discr_5 := Lean.Syntax.getArg discr 2; let discr_6 := Lean.Syntax.getArg discr 3; let discr_7 := Lean.Syntax.getArg discr 4; let discr_8 := Lean.Syntax.getArg discr 5; let discr_9 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr_2 := Lean.Syntax.getArg discr 0; let discr_3 := Lean.Syntax.getArg discr 1; let discr_4 := Lean.Syntax.getArg discr 2; let discr_5 := Lean.Syntax.getArg discr 3; let discr_6 := Lean.Syntax.getArg discr 4; let discr_7 := Lean.Syntax.getArg discr 5; let discr_8 := Lean.Syntax.getArg discr 6; let discr := Lean.Syntax.getArg discr 7; Lean.Macro.throwUnsupported else let discr := stx; Lean.Macro.throwUnsupported) Lean.Elab.Command.expandMixfix.withAttrKindGlobal
def
Lean.Elab.Command.expandMixfix.withAttrKindGlobal
(stx : Lean.Syntax)
(f : Lean.Syntax → Lean.MacroM Lean.Syntax)
:
Equations
- Lean.Elab.Command.expandMixfix.withAttrKindGlobal stx f = let attrKind := Lean.Syntax.getOp stx 0; let stx := Lean.Syntax.setArg stx 0 Lean.Elab.mkAttrKindGlobal; do let stx ← f stx pure (Lean.Syntax.setArg stx 0 attrKind)