Equations
- Lean.Elab.Command.expandNotationItemIntoSyntaxItem stx = let k := Lean.Syntax.getKind stx; if (k == `Lean.Parser.Command.identPrec) = true then pure (Lean.mkNode `Lean.Parser.Syntax.cat #[Lean.mkIdentFrom stx `term, Lean.Syntax.getOp stx 1]) else if (k == Lean.strLitKind) = true then pure (Lean.mkNode `Lean.Parser.Syntax.atom #[stx]) else Lean.Macro.throwUnsupported
Equations
- Lean.Elab.Command.expandNotationItemIntoPattern stx = let k := Lean.Syntax.getKind stx; if (k == `Lean.Parser.Command.identPrec) = true then pure (Lean.Syntax.mkAntiquotNode (Lean.Syntax.getOp stx 0) 0 none) else if (k == Lean.strLitKind) = true then Lean.Elab.Command.strLitToPattern stx else Lean.Macro.throwUnsupported
def
Lean.Elab.Command.mkSimpleDelab
(attrKind : Lean.Syntax)
(vars : Array Lean.Syntax)
(pat : Lean.Syntax)
(qrhs : Lean.Syntax)
:
Equations
- Lean.Elab.Command.mkSimpleDelab attrKind vars pat qrhs = let discr := qrhs; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; cond (Lean.Syntax.isOfKind discr_1 `ident) (let discr := Lean.Syntax.getArg discr 1; let args := Lean.Syntax.getArgs discr; let c := discr_1; do let discr ← liftM (Lean.Macro.resolveGlobalName (Lean.Syntax.getId c)) match discr with | [(c, [])] => do guard (Array.all args (Lean.Syntax.isIdent ∘ Lean.Syntax.getAntiquotTerm) 0 (Array.size args) = true) guard (Array.allDiff args = true) let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Elab.Command.aux_def #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attributes #[Lean.Syntax.atom info "@[", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrInstance #[attrKind, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Attr.simple #[Lean.Syntax.ident info (String.toSubstring "appUnexpander") (Lean.addMacroScope mainModule `appUnexpander scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.mkIdent c]]]], Lean.Syntax.atom info "]"]], Lean.Syntax.atom info "aux_def", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "unexpand") (Lean.addMacroScope mainModule `unexpand scp) [], Lean.mkIdent c], Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "Lean.PrettyPrinter.Unexpander") (Lean.addMacroScope mainModule `Lean.PrettyPrinter.Unexpander scp) [(`Lean.PrettyPrinter.Unexpander, [])], Lean.Syntax.atom info ":=", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.quot #[Lean.Syntax.atom info "`(", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.node Lean.SourceInfo.none `ident.antiquot #[Lean.Syntax.atom info "$", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.ident info (String.toSubstring "f") (Lean.addMacroScope mainModule `f scp) [], Lean.Syntax.node Lean.SourceInfo.none `antiquotName #[Lean.Syntax.atom info ":", Lean.Syntax.atom info "ident"]], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] args)], Lean.Syntax.atom info ")"]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "withRef") (Lean.addMacroScope mainModule `withRef scp) [(`Lean.withRef, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "f") (Lean.addMacroScope mainModule `f scp) [], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.quot #[Lean.Syntax.atom info "`(", pat, Lean.Syntax.atom info ")"]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "throw") (Lean.addMacroScope mainModule `throw scp) [(`MonadExcept.throw, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ")"]]]]]]]]) | x => failure) (let discr_2 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; failure) else let discr := qrhs; cond (Lean.Syntax.isOfKind discr `ident) (let c := discr; do let discr ← liftM (Lean.Macro.resolveGlobalName (Lean.Syntax.getId c)) match discr with | [(c, [])] => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Elab.Command.aux_def #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attributes #[Lean.Syntax.atom info "@[", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrInstance #[attrKind, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Attr.simple #[Lean.Syntax.ident info (String.toSubstring "appUnexpander") (Lean.addMacroScope mainModule `appUnexpander scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.mkIdent c]]]], Lean.Syntax.atom info "]"]], Lean.Syntax.atom info "aux_def", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "unexpand") (Lean.addMacroScope mainModule `unexpand scp) [], Lean.mkIdent c], Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "Lean.PrettyPrinter.Unexpander") (Lean.addMacroScope mainModule `Lean.PrettyPrinter.Unexpander scp) [(`Lean.PrettyPrinter.Unexpander, [])], Lean.Syntax.atom info ":=", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.quot #[Lean.Syntax.atom info "`(", Lean.Syntax.node Lean.SourceInfo.none `ident.antiquot #[Lean.Syntax.atom info "$", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.ident info (String.toSubstring "f") (Lean.addMacroScope mainModule `f scp) [], Lean.Syntax.node Lean.SourceInfo.none `antiquotName #[Lean.Syntax.atom info ":", Lean.Syntax.atom info "ident"]], Lean.Syntax.atom info ")"]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "withRef") (Lean.addMacroScope mainModule `withRef scp) [(`Lean.withRef, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "f") (Lean.addMacroScope mainModule `f scp) [], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.quot #[Lean.Syntax.atom info "`(", pat, Lean.Syntax.atom info ")"]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "throw") (Lean.addMacroScope mainModule `throw scp) [(`MonadExcept.throw, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ")"]]]]]]]]) | x => failure) (let discr := qrhs; failure)
Equations
- Lean.Elab.Command.expandNotation x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.notation = true then let discr_1 := Lean.Syntax.getArg discr 0; cond (Lean.Syntax.isOfKind discr_1 `Lean.Parser.Term.attrKind) (let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; let yes := fun x prec? => let discr_4 := Lean.Syntax.getArg discr 3; let yes := fun x name? => let discr_5 := Lean.Syntax.getArg discr 4; let yes := fun x prio? => let discr_6 := Lean.Syntax.getArg discr 5; let discr_7 := Lean.Syntax.getArg discr 6; let discr_8 := Lean.Syntax.getArg discr 7; let rhs := discr_8; let items := Lean.Syntax.getArgs discr_6; let attrKind := discr_1; let stx := discr; do let discr ← Lean.Elab.toAttributeKind attrKind let x : Lean.AttributeKind := discr match x with | x => do let a ← Lean.Macro.getCurrNamespace Lean.Elab.Command.expandNotationAux stx a attrKind prec? name? prio? items rhs; if Lean.Syntax.isNone discr_5 = true then yes () none else let discr_6 := discr_5; if Lean.Syntax.matchesNull discr_6 1 = true then let discr_7 := Lean.Syntax.getArg discr_6 0; if Lean.Syntax.isOfKind discr_7 `Lean.Parser.Command.namedPrio = true then let discr := Lean.Syntax.getArg discr_7 0; let discr := Lean.Syntax.getArg discr_7 1; let discr := Lean.Syntax.getArg discr_7 2; let discr := Lean.Syntax.getArg discr_7 3; let discr_8 := Lean.Syntax.getArg discr_7 4; let prio? := discr; yes () (some prio?) else let discr_8 := Lean.Syntax.getArg discr_6 0; 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_7 := discr_5; 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; if Lean.Syntax.isNone discr_4 = true then yes () none else let discr_5 := discr_4; if Lean.Syntax.matchesNull discr_5 1 = true then let discr_6 := Lean.Syntax.getArg discr_5 0; if Lean.Syntax.isOfKind discr_6 `Lean.Parser.Command.namedName = true then let discr := Lean.Syntax.getArg discr_6 0; let discr := Lean.Syntax.getArg discr_6 1; let discr := Lean.Syntax.getArg discr_6 2; let discr := Lean.Syntax.getArg discr_6 3; let discr_7 := Lean.Syntax.getArg discr_6 4; let name? := discr; yes () (some name?) else let discr_7 := Lean.Syntax.getArg discr_5 0; 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_6 := discr_4; 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; if Lean.Syntax.isNone discr_3 = true then yes () none else let discr_4 := discr_3; if Lean.Syntax.matchesNull discr_4 1 = true then let discr_5 := Lean.Syntax.getArg discr_4 0; if Lean.Syntax.isOfKind discr_5 `Lean.Parser.precedence = true then let discr := Lean.Syntax.getArg discr_5 0; let discr := Lean.Syntax.getArg discr_5 1; let prec? := discr; yes () (some prec?) else let discr_6 := Lean.Syntax.getArg discr_4 0; 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 := discr_3; 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) (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 := x; Lean.Macro.throwUnsupported