diff --git a/tests/lean/lisp.lean.expected.out b/tests/lean/lisp.lean.expected.out deleted file mode 100644 index ba3a690d09..0000000000 --- a/tests/lean/lisp.lean.expected.out +++ /dev/null @@ -1,20 +0,0 @@ -lisp.lean:200:0: error: cannot evaluate (list "(" [] ")") -reader: (list "(" [] ")") -expander: (list "(" [] ")") -resolver: (list "(" [] ")") -reader: (list "(" [(list "(" [lambda (list "[" [x] "]") x] ")") 1] ")") -expander: (list "(" [(lambda_core (bind [x] x)) 1] ")") -resolver: (list "(" [(lambda_core (bind [x] x:0)) 1] ")") -evaluator: 1 -reader: (list "(" [(list "(" [lambda (list "[" [x y] "]") x] ")") 1 2] ")") -expander: (list "(" [(lambda_core (bind [x] (lambda_core (bind [y] x)))) 1 2] ")") -resolver: (list "(" [(lambda_core (bind [x] (lambda_core (bind [y] x:1)))) 1 2] ")") -evaluator: 1 -reader: (list "(" [let (list "(" [(list "[" [x 1] "]")] ")") x] ")") -expander: (let_core [1] (bind [x] x)) -resolver: (let_core [1] (bind [x] x:0)) -evaluator: 1 -reader: (list "(" [let (list "(" [(list "[" [tmp 5] "]")] ")") (list "(" [or 0 tmp] ")")] ")") -expander: (let_core [5] (bind [tmp] (let_core [0] (bind [tmp!3] (if tmp!3 tmp!3 tmp))))) -resolver: (let_core [5] (bind [tmp] (let_core [0] (bind [tmp!3] (if tmp!3:0 tmp!3:0 tmp:1))))) -evaluator: 5 diff --git a/tests/lean/macro1.lean.expected.out b/tests/lean/macro1.lean.expected.out deleted file mode 100644 index 92cff6e943..0000000000 --- a/tests/lean/macro1.lean.expected.out +++ /dev/null @@ -1,4 +0,0 @@ -(lambda_core (bind [x] x:0)) -macro1.lean:49:0: error: unknown identifier y -(lambda_core (bind [x] (lambda_core (bind [x!1] x:1)))) -(lambda_core (bind [x.y] x.y.z:0.(z))) diff --git a/tests/lean/reader1.lean.expected.out b/tests/lean/reader1.lean.expected.out deleted file mode 100644 index 7d738d4847..0000000000 --- a/tests/lean/reader1.lean.expected.out +++ /dev/null @@ -1,764 +0,0 @@ -result: -[(lean.parser.reader.module [(lean.parser.reader.prelude "prelude")] [] []) - (lean.parser.reader.eoi "")] -result: -[(lean.parser.reader.module - [] - [(lean.parser.reader.import "import" [(lean.parser.reader.import_path [] me)])] - []) - (lean.parser.reader.eoi "")] -error at line 1, column 0: -expected command -partial syntax tree: -[(lean.parser.reader.module [] [] []) (lean.parser.reader.eoi "")] -error at line 1, column 6: -expected "." or identifier -partial syntax tree: -[(lean.parser.reader.module - [] - [(lean.parser.reader.import - "import" - [(lean.parser.reader.import_path [] ) ]) - ] - ) - (lean.parser.reader.eoi "")] -result: -[(lean.parser.reader.module - [(lean.parser.reader.prelude "prelude")] - [(lean.parser.reader.import - "import" - [(lean.parser.reader.import_path ["." "."] a) - (lean.parser.reader.import_path [] b)]) - (lean.parser.reader.import "import" [(lean.parser.reader.import_path [] c)])] - []) - (lean.parser.reader.eoi "")] -result: -[(lean.parser.reader.module - [] - [] - [(lean.parser.reader.open - "open" - [(lean.parser.reader.open_spec me [] [] [] []) - (lean.parser.reader.open_spec you [] [] [] [])])]) - (lean.parser.reader.eoi "")] -result: -[(lean.parser.reader.module - [] - [] - [(lean.parser.reader.open - "open" - [(lean.parser.reader.open_spec - me - [(lean.parser.reader.open_spec.as "as" you)] - [(lean.parser.reader.open_spec.only ["(" a] [b c] ")")] - [(lean.parser.reader.open_spec.renaming - ["(" "renaming"] - [(lean.parser.reader.open_spec.renaming.item a "->" b) - (lean.parser.reader.open_spec.renaming.item c "->" d)] - ")")] - [(lean.parser.reader.open_spec.hiding "(" "hiding" [a b] ")")])])]) - (lean.parser.reader.eoi "")] -error at line 1, column 8: -expected command -partial syntax tree: -[(lean.parser.reader.module - [] - [] - [(lean.parser.reader.open "open" [(lean.parser.reader.open_spec me [] [] [] [])])]) - (lean.parser.reader.eoi "")] -error at line 1, column 5: -expected identifier -error at line 1, column 9: -expected identifier -partial syntax tree: -[(lean.parser.reader.module - [] - [] - [(lean.parser.reader.open - "open" - [(lean.parser.reader.open_spec ) - ]) - (lean.parser.reader.open - "open" - [(lean.parser.reader.open_spec ) - ])]) - (lean.parser.reader.eoi "")] -error at line 1, column 8: -expected command -partial syntax tree: -[(lean.parser.reader.module - [] - [] - [(lean.parser.reader.open "open" [(lean.parser.reader.open_spec me [] [] [] [])]) - (lean.parser.reader.open - "open" - [(lean.parser.reader.open_spec you [] [] [] [])])]) - (lean.parser.reader.eoi "")] -result: -[(lean.parser.reader.module - [] - [] - [(lean.parser.reader.open "open" [(lean.parser.reader.open_spec a [] [] [] [])]) - (lean.parser.reader.section - "section" - [b] - [(lean.parser.reader.open "open" [(lean.parser.reader.open_spec c [] [] [] [])]) - (lean.parser.reader.section - "section" - [d] - [(lean.parser.reader.open "open" [(lean.parser.reader.open_spec e [] [] [] [])])] - "end" - [d])] - "end" - [b])]) - (lean.parser.reader.eoi "")] -result: -[(lean.parser.reader.module - [] - [] - [(lean.parser.reader.section "section" [a] [] "end" [])]) - (lean.parser.reader.eoi "")] -result: -[(lean.parser.reader.module - [] - [] - [(lean.parser.reader.notation - "notation" - (lean.parser.reader.notation_spec - (1 - (lean.parser.reader.notation_spec.rules - [] - [(lean.parser.reader.notation_spec.rule - (lean.parser.reader.notation_spec.notation_symbol - (0 (lean.parser.reader.notation_spec.notation_quoted_symbol "`" "Prop" "`" []))) - [])]))) - ":=" - (lean.parser.reader.hole "_"))]) - (lean.parser.reader.eoi "")] -(lean.parser.reader.notation - "notation" - (lean.parser.reader.notation_spec - (1 - (lean.parser.reader.notation_spec.rules - [] - [(lean.parser.reader.notation_spec.rule - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "+" - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "10"))]))) - [(lean.parser.reader.notation_spec.transition - (2 - (lean.parser.reader.notation_spec.argument - b - [(lean.parser.reader.notation_spec.action - ":" - (lean.parser.reader.notation_spec.action_kind - (0 (lean.parser.reader.base10_lit "10"))))])))])]))) - ":=" - (lean.parser.reader.hole "_")) -notation`+`:10 b:10 :=_ -error at line 10, column 19: -expected "_" -error at line 11, column 26: -expected "_" -error at line 85, column 0: -expected command -partial syntax tree: -[(lean.parser.reader.module - [(lean.parser.reader.prelude "prelude")] - [] - [(lean.parser.reader.notation - "notation" - (lean.parser.reader.notation_spec - (1 - (lean.parser.reader.notation_spec.rules - [] - [(lean.parser.reader.notation_spec.rule - (lean.parser.reader.notation_spec.notation_symbol - (0 (lean.parser.reader.notation_spec.notation_quoted_symbol "`" "Prop" "`" []))) - [])]))) - ":=" - (lean.parser.reader.hole )) - (lean.parser.reader.notation - "notation" - (lean.parser.reader.notation_spec - (1 - (lean.parser.reader.notation_spec.rules - [f] - [(lean.parser.reader.notation_spec.rule - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "$ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "1"))]))) - [(lean.parser.reader.notation_spec.transition - (2 - (lean.parser.reader.notation_spec.argument - a - [(lean.parser.reader.notation_spec.action - ":" - (lean.parser.reader.notation_spec.action_kind - (0 (lean.parser.reader.base10_lit "0"))))])))])]))) - ":=" - (lean.parser.reader.hole )) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (0 "prefix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "¬" - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "40"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (0 "prefix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "~" - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "40"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (3 "infixr"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "∧ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "35"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (3 "infixr"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "/\\ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "35"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (3 "infixr"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "\\/ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "30"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (3 "infixr"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "∨ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "30"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "<-> " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "20"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "↔ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "20"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "= " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "== " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "≠ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "≈ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "~ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "≡ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (2 "infixl"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "⬝ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "75"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (3 "infixr"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "▸ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "75"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (3 "infixr"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "▹ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "75"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (3 "infixr"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "⊕ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "30"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (3 "infixr"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "× " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "35"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (2 "infixl"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "+ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "65"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (2 "infixl"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "- " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "65"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (2 "infixl"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "* " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "70"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (2 "infixl"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "/ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "70"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (2 "infixl"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "% " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "70"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (2 "infixl"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "%ₙ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "70"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (0 "prefix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "-" - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "100"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (3 "infixr"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "^ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "80"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (3 "infixr"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "∘ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "90"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "<= " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "≤ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "< " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - ">= " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "≥ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "> " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (0 "prefix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "!" - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "40"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (2 "infixl"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "&& " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "35"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (2 "infixl"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "|| " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "30"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "∈ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "∉ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (2 "infixl"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "∩ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "70"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (2 "infixl"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "∪ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "65"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "⊆ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "⊇ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "⊂ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "⊃ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "\\ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "70"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (1 "infix"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "∣ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "50"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (2 "infixl"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "++ " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "65"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (3 "infixr"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - ":: " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "67"))])))) - (lean.parser.reader.reserve_mixfix - ["reserve" (lean.parser.reader.mixfix.kind (2 "infixl"))] - (lean.parser.reader.notation_spec.notation_symbol - (0 - (lean.parser.reader.notation_spec.notation_quoted_symbol - "`" - "; " - "`" - [(lean.parser.reader.notation_spec.precedence - ":" - (lean.parser.reader.base10_lit "1"))])))) - (lean.parser.reader.universes "universes" [u v w])]) - (lean.parser.reader.eoi "")]