From fa0148e5b84fcc61e3ee670af79126c27aa43cb3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 17 Sep 2018 17:47:53 -0700 Subject: [PATCH] feat(library/init/lean/parser): declarations and binders --- library/init/lean/parser/basic.lean | 12 + library/init/lean/parser/combinators.lean | 83 ++- library/init/lean/parser/command.lean | 7 +- library/init/lean/parser/declaration.lean | 81 +++ library/init/lean/parser/notation.lean | 32 +- library/init/lean/parser/term.lean | 70 +- library/init/lean/parser/token.lean | 1 - tests/lean/parser1.lean.expected.out | 820 ++++++++++++---------- 8 files changed, 693 insertions(+), 413 deletions(-) create mode 100644 library/init/lean/parser/declaration.lean diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean index a8e0a50571..4d5b214e7c 100644 --- a/library/init/lean/parser/basic.lean +++ b/library/init/lean/parser/basic.lean @@ -48,6 +48,7 @@ structure parser_config := def parser_t (m : Type → Type) [monad m] := reader_t parser_config $ state_t parser_state $ parsec_t syntax m abbreviation basic_parser_m := parser_t id abbreviation basic_parser := basic_parser_m syntax +abbreviation monad_basic_read := has_monad_lift_t basic_parser_m -- an arbitrary `parser` type; parsers are usually some monad stack based on `basic_parser_m` returning `syntax` variable {ρ : Type} @@ -125,5 +126,16 @@ def parse.view : syntax → option parse.view_ty | (syntax.node ⟨none, [root, eoi]⟩) := some ⟨root, eoi⟩ | _ := none + +/- Monad stacks used in multiple files -/ + +@[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_rec monad_basic_read] +def command_parser_m := rec_t unit syntax basic_parser_m +abbreviation command_parser := command_parser_m syntax + +@[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_rec monad_basic_read] +def term_parser_m := rec_t nat syntax command_parser_m +abbreviation term_parser := term_parser_m syntax + end «parser» end lean diff --git a/library/init/lean/parser/combinators.lean b/library/init/lean/parser/combinators.lean index f3ad6e5ac4..1287815414 100644 --- a/library/init/lean/parser/combinators.lean +++ b/library/init/lean/parser/combinators.lean @@ -10,6 +10,9 @@ import init.lean.parser.basic namespace lean namespace parser + +@[pattern] def choice := {syntax_node_kind . name := `lean.parser.choice} + namespace combinators open has_tokens has_view monad_parsec @@ -39,10 +42,11 @@ instance node.view (k) (rs : list parser) [i : syntax_node_kind.has_view k α] : private def many1_aux (p : parser) : list syntax → nat → parser | as 0 := error "unreachable" -| as (n+1) := do a ← catch p (λ msg, throw {msg with custom := - -- append `syntax.missing` to make clear that list is incomplete - syntax.node ⟨none, (syntax.missing::msg.custom::as).reverse⟩}), - many1_aux (a::as) n <|> pure (syntax.node ⟨none, (a::as).reverse⟩) +| as (n+1) := do + a ← catch p (λ msg, throw {msg with custom := + -- append `syntax.missing` to make clear that list is incomplete + syntax.node ⟨none, (syntax.missing::msg.custom::as).reverse⟩}), + many1_aux (a::as) n <|> pure (syntax.node ⟨none, (a::as).reverse⟩) def many1 (r : parser) : parser := do rem ← remaining, many1_aux r [] (rem+1) @@ -66,6 +70,59 @@ instance many.tokens (r : parser) [parser.has_tokens r] : parser.has_tokens (man instance many.view (r : parser) [has_view r α] : parser.has_view (many r) (list α) := {..many1.view r} +private def sep_by_aux (p : m syntax) (sep : parser) (allow_trailing_sep : bool) : bool → list syntax → nat → parser +| p_opt as 0 := error "unreachable" +| p_opt as (n+1) := do + let p := if p_opt then some <$> p <|> pure none else some <$> p, + some a ← catch p (λ msg, throw {msg with custom := + -- append `syntax.missing` to make clear that list is incomplete + syntax.node ⟨none, (syntax.missing::msg.custom::as).reverse⟩}) + | pure (syntax.node ⟨none, as.reverse⟩), + -- I don't want to think about what the output on a failed separator parse should look like + let sep := try sep, + some s ← some <$> sep <|> pure none + | pure (syntax.node ⟨none, (a::as).reverse⟩), + sep_by_aux allow_trailing_sep (s::a::as) n + +def sep_by (p sep : parser) (allow_trailing_sep := tt) : parser := +do rem ← remaining, sep_by_aux p sep allow_trailing_sep tt [] (rem+1) + +def sep_by1 (p sep : parser) (allow_trailing_sep := tt) : parser := +do rem ← remaining, sep_by_aux p sep allow_trailing_sep ff [] (rem+1) + +instance sep_by.tokens (p sep : parser) (a) [parser.has_tokens p] [parser.has_tokens sep] : + parser.has_tokens (sep_by p sep a) := +⟨tokens p ++ tokens sep⟩ + +private def sep_by.view_aux {α β} (p sep : parser) [parser.has_view p α] [parser.has_view sep β] : + list syntax → option (list (α × option β)) +| [] := some [] +| [stx] := do + vp ← view p stx, + some [(vp, none)] +| (stx1::stx2::stxs) := do + vp ← view p stx1, + vsep ← view sep stx2, + vs ← sep_by.view_aux stxs, + some ((vp, some vsep)::vs) + +instance sep_by.view {α β} (p sep : parser) (a) [parser.has_view p α] [parser.has_view sep β] : + parser.has_view (sep_by p sep a) (list (α × option β)) := +{ view := λ stx, match stx with + | syntax.node ⟨none, stxs⟩ := sep_by.view_aux p sep stxs + | _ := failure, + review := λ as, syntax.node ⟨none, as.bind (λ a, match a with + | ⟨v, some vsep⟩ := [review p v, review sep vsep] + | ⟨v, none⟩ := [review p v])⟩ } + +instance sep_by1.tokens (p sep : parser) (a) [parser.has_tokens p] [parser.has_tokens sep] : + parser.has_tokens (sep_by1 p sep a) := +⟨tokens (sep_by p sep a)⟩ + +instance sep_by1.view {α β} (p sep : parser) (a) [parser.has_view p α] [parser.has_view sep β] : + parser.has_view (sep_by1 p sep a) (list (α × option β)) := +{..sep_by.view p sep a} + def optional (r : parser) : parser := do r ← optional $ -- on error, wrap in "some" @@ -111,9 +168,20 @@ match rs with instance any_of.tokens (rs : list parser) [parser.has_tokens rs] : parser.has_tokens (any_of rs) := ⟨tokens rs⟩ - instance any_of.view (rs : list parser) : parser.has_view (any_of rs) syntax := default _ +/-- Parse a list `[p1, ..., pn]` of parsers with `monad_parsec.longest_match`. + If the result is ambiguous, wrap it in a `choice` node. + Note that there is NO explicit encoding of which parser was chosen; + parsers should instead produce distinct node names for disambiguation. -/ +def longest_match (rs : list parser) : parser := +do stxs ← monad_parsec.longest_match rs, + pure $ syntax.node ⟨choice, stxs⟩ + +instance longest_match.tokens (rs : list parser) [parser.has_tokens rs] : parser.has_tokens (longest_match rs) := +⟨tokens rs⟩ +instance longest_match.view (rs : list parser) : parser.has_view (longest_match rs) syntax := default _ + /-- Parse a list `[p1, ..., pn]` of parsers as `p1 <|> ... <|> pn`. The result will be wrapped in a node with the the index of the successful parser as the name. -/ @@ -172,6 +240,11 @@ instance seq_right.tokens {α : Type} (x : m α) (p : m syntax) [parser.has_toke instance seq_right.view {α β : Type} (x : m α) (p : m syntax) [i : parser.has_view p β] : parser.has_view (x *> p) β := {..i} +instance coe.tokens {β} (r : parser) [parser.has_tokens r] [has_coe_t parser β]: parser.has_tokens (coe r : β) := +⟨tokens r⟩ +instance coe.view {β} (r : parser) [i : parser.has_view r α] [has_coe_t parser β] : parser.has_view (coe r : β) α := +{..i} + end combinators end parser end lean diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean index fcd864f2b3..5302bf6e24 100644 --- a/library/init/lean/parser/command.lean +++ b/library/init/lean/parser/command.lean @@ -6,7 +6,7 @@ Author: Sebastian Ullrich Command parsers -/ prelude -import init.lean.parser.notation +import init.lean.parser.declaration namespace lean namespace parser @@ -21,9 +21,10 @@ local postfix +:10000 := combinators.many1 @[derive parser.has_view parser.has_tokens] def command_parser.recurse : command_parser := recurse () +set_option class.instance_max_depth 200 + namespace «command» -set_option class.instance_max_depth 200 @[derive parser.has_view parser.has_tokens] def open_spec.parser : command_parser := node! open_spec [ @@ -62,7 +63,7 @@ open «command» @[derive parser.has_tokens parser.has_view] def command.parser : command_parser := any_of [open.parser, section.parser, universe.parser, notation.parser, reserve_notation.parser, - mixfix.parser, reserve_mixfix.parser, check.parser] "command" + mixfix.parser, reserve_mixfix.parser, check.parser, declaration.parser] "command" end parser diff --git a/library/init/lean/parser/declaration.lean b/library/init/lean/parser/declaration.lean new file mode 100644 index 0000000000..37e3a5e405 --- /dev/null +++ b/library/init/lean/parser/declaration.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2018 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Sebastian Ullrich + +Parsers for commands that declare things +-/ + +prelude +import init.lean.parser.term + +namespace lean +namespace parser + +open combinators monad_parsec +open parser.has_tokens parser.has_view + +instance term_parser_command_parser_coe : has_coe term_parser command_parser := +-- run `p` directly, but use the general `term.parser` for recursion +⟨λ p, reader_t.run p $ λ rbp, term.parser rbp⟩ + +namespace «command» + +local postfix `?`:10000 := optional +local postfix *:10000 := combinators.many +local postfix +:10000 := combinators.many1 + +@[derive has_tokens has_view] +def attr_instance.parser : command_parser := +node! attr_instance [name: ident.parser, args: term.parser*] + +@[derive has_tokens has_view] +def decl_attributes.parser : command_parser := +-- TODO(Seabstian): custom attribute parsers +node! decl_attribute ["@[", attrs: sep_by1 attr_instance.parser (symbol ","), "]"] + +set_option class.instance_max_depth 200 +@[derive has_tokens has_view] +def decl_modifiers.parser : command_parser := +node! decl_modifiers [ + visibility: node_choice! visibility {"private", "protected"}?, + «noncomputable»: (symbol "noncomputable")?, + «meta»: (symbol "meta")?, + attrs: decl_attributes.parser? +] + +@[derive has_tokens has_view] +def decl_sig.parser : command_parser := +node! decl_sig [ + params: term.bracketed_binder.parser*, + type: node! decl_type [":", type: term.parser]? +] + +@[derive has_tokens has_view] +def equation.parser : command_parser := +node! equation ["|", lhs: term.parser, ":=", rhs: term.parser] + +@[derive has_tokens has_view] +def decl_val.parser : command_parser := +node_choice! decl_val { + simple: node! simple_decl_val [":=", body: term.parser], + empty_match: symbol ".", + «match»: equation.parser+ +} + +@[derive has_tokens has_view] +def declaration.parser : command_parser := +node! declaration [ + modifiers: decl_modifiers.parser, + inner: node_choice! declaration.inner { + «def»: node! «def» ["def", name: ident.parser, sig: decl_sig.parser, val: decl_val.parser], + «abbreviation»: node! «abbreviation» ["abbreviation", name: ident.parser, sig: decl_sig.parser, val: decl_val.parser], + «theorem»: node! «theorem» ["theorem", name: ident.parser, sig: decl_sig.parser, val: decl_val.parser], + «instance»: node! «instance» ["instance", name: ident.parser?, sig: decl_sig.parser, val: decl_val.parser], + «example»: node! «example» ["example", sig: decl_sig.parser, val: decl_val.parser], + } +] + +end «command» +end parser +end lean diff --git a/library/init/lean/parser/notation.lean b/library/init/lean/parser/notation.lean index 52b2af5bfb..55988ae365 100644 --- a/library/init/lean/parser/notation.lean +++ b/library/init/lean/parser/notation.lean @@ -6,7 +6,7 @@ Author: Sebastian Ullrich Notation parsers -/ prelude -import init.lean.parser.term +import init.lean.parser.token namespace lean namespace parser @@ -23,10 +23,10 @@ set_option class.instance_max_depth 100 namespace notation_spec @[derive parser.has_tokens parser.has_view] -def precedence.parser : command_parser := +def precedence.parser : term_parser := node! «precedence» [":", prec: number]/-TODO <|> expr-/ -def quoted_symbol.parser : command_parser := +def quoted_symbol.parser : term_parser := do (s, info) ← with_source_info $ take_until (= '`'), pure $ syntax.atom ⟨info, s⟩ @@ -34,7 +34,7 @@ instance quoted_symbol.tokens : parser.has_tokens quoted_symbol.parser := ⟨[] instance quoted_symbol.view : parser.has_view quoted_symbol.parser syntax := default _ @[derive parser.has_tokens parser.has_view] -def symbol_quote.parser : command_parser := +def symbol_quote.parser : term_parser := node! notation_quoted_symbol [ left_quote: raw $ ch '`', symbol: quoted_symbol.parser, @@ -43,14 +43,14 @@ node! notation_quoted_symbol [ --TODO(Sebastian): cannot be called `symbol` because of hygiene problems @[derive parser.has_tokens parser.has_view] -def notation_symbol.parser : command_parser := +def notation_symbol.parser : term_parser := node_choice! notation_symbol { quoted: symbol_quote.parser --TODO, {read := do tk ← token, /- check if reserved token-/} } @[derive parser.has_tokens parser.has_view] -def action.parser : command_parser := +def action.parser : term_parser := node! action [":", action: node_choice! action_kind { prec: number, max: symbol_or_ident "max", @@ -63,7 +63,7 @@ node! action [":", action: node_choice! action_kind { notation_tk,-/}] @[derive parser.has_tokens parser.has_view] -def transition.parser : command_parser := +def transition.parser : term_parser := node_choice! transition { binder: node! binder ["binder", prec: precedence.parser?], binders: node! binders ["binders", prec: precedence.parser?], @@ -71,38 +71,38 @@ node_choice! transition { } @[derive parser.has_tokens parser.has_view] -def rule.parser : command_parser := +def rule.parser : term_parser := node! rule [symbol: notation_symbol.parser, transition: transition.parser?] end notation_spec @[derive parser.has_tokens parser.has_view] -def notation_spec.parser : command_parser := +def notation_spec.parser : term_parser := node_choice! notation_spec { number_literal: number, rules: node! notation_spec.rules [id: ident.parser?, rules: notation_spec.rule.parser*] } @[derive parser.has_tokens parser.has_view] -def notation.parser : command_parser := -node! «notation» ["notation", spec: notation_spec.parser, ":=", term: term.parser] +def notation.parser : term_parser := +node! «notation» ["notation", spec: notation_spec.parser, ":=", term: recurse 0] @[derive parser.has_tokens parser.has_view] -def reserve_notation.parser : command_parser := +def reserve_notation.parser : term_parser := node! «reserve_notation» [try ["reserve", "notation"], spec: notation_spec.parser] @[derive parser.has_tokens parser.has_view] -def mixfix.kind.parser : command_parser := +def mixfix.kind.parser : term_parser := node_choice! mixfix.kind {"prefix", "infix", "infixl", "infixr", "postfix"} @[derive parser.has_tokens parser.has_view] -def mixfix.parser : command_parser := +def mixfix.parser : term_parser := node! «mixfix» [ kind: mixfix.kind.parser, - symbol: notation_spec.notation_symbol.parser, ":=", term: term.parser] + symbol: notation_spec.notation_symbol.parser, ":=", term: recurse 0] @[derive parser.has_tokens parser.has_view] -def reserve_mixfix.parser : command_parser := +def reserve_mixfix.parser : term_parser := node! «reserve_mixfix» [ try ["reserve", kind: mixfix.kind.parser], symbol: notation_spec.notation_symbol.parser] diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index bb704ddba4..2896bcacaf 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -6,7 +6,7 @@ Author: Sebastian Ullrich Term-level parsers -/ prelude -import init.lean.parser.level +import init.lean.parser.level init.lean.parser.notation namespace lean namespace parser @@ -16,20 +16,12 @@ local postfix `?`:10000 := optional local postfix *:10000 := combinators.many local postfix +:10000 := combinators.many1 -@[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_rec monad_basic_read] -def command_parser_m := rec_t unit syntax basic_parser_m -abbreviation command_parser := command_parser_m syntax - -@[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_rec monad_basic_read] -def term_parser_m := rec_t nat syntax command_parser_m -abbreviation term_parser := term_parser_m syntax /-- A term parser for a suffix or infix notation that accepts a preceding term. -/ @[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_rec monad_basic_read] def trailing_term_parser_m := reader_t syntax term_parser_m abbreviation trailing_term_parser := trailing_term_parser_m syntax - @[derive parser.has_tokens parser.has_view] def ident_univ_spec.parser : basic_parser := node! ident_univ_spec [".{", levels: level.parser+, "}"] @@ -52,6 +44,66 @@ node! hole [hole: symbol "_" max_prec] def sort.parser : term_parser := node_choice! sort {"Sort":max_prec, "Type":max_prec} +set_option class.instance_max_depth 200 + +section binder +@[derive has_tokens has_view] +def binder_content.parser : term_parser := +node! binder_content [ + ids: (node_choice! binder_id {id: ident.parser, hole: hole.parser})+, + type: node! binder_content_type [":", type: recurse 0], + default: node_choice! binder_default { + val: node! binder_default_val [":=", term: recurse 0], + tac: node! binder_default_tac [".", term: recurse 0] + }? +] + +/- All binders must be surrounded with some kind of bracket. (e.g., '()', '{}', '[]'). + We use this feature when parsing examples/definitions/theorems. The goal is to avoid counter-intuitive + declarations such as: + + example p : false := trivial + def main proof : false := trivial + + which would be parsed as + + example (p : false) : _ := trivial + + def main (proof : false) : _ := trivial + + where `_` in both cases is elaborated into `true`. This issue was raised by @gebner in the slack channel. + + + Remark: we still want implicit delimiters for lambda/pi expressions. That is, we want to + write + + fun x : t, s + or + fun x, s + + instead of + + fun (x : t), s -/ +@[derive has_tokens has_view] +def bracketed_binder.parser : term_parser := +node_choice! bracketed_binder { + explicit: node! explicit_binder ["(":max_prec, content: node_choice! explicit_binder_content { + «notation»: any_of [command.notation.parser, command.mixfix.parser], + other: binder_content.parser + }, right: symbol ")"], + implicit: node! implicit_binder ["{":max_prec, content: binder_content.parser, "}"], + strict_implicit: node! strict_implicit_binder [ + left: any_of [symbol "{{" max_prec, symbol "⦃" max_prec], + content: binder_content.parser, + right: any_of [symbol "}}", symbol "⦄"] + ], + inst_implicit: node! inst_implicit_binder ["[":max_prec, content: longest_match [ + node! inst_implicit_named_binder [id: ident.parser, type: recurse 0], + node! inst_implicit_anonymous_binder [type: recurse 0] + ], "]"] +} +end binder + @[derive parser.has_tokens parser.has_view] def leading.parser := any_of [ diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean index 2cb561188f..62d4ca928c 100644 --- a/library/init/lean/parser/token.lean +++ b/library/init/lean/parser/token.lean @@ -46,7 +46,6 @@ do whitespace, pure () | 0 := error "unreachable" -abbreviation monad_basic_read := has_monad_lift_t basic_parser_m variables {m : Type → Type} local notation `parser` := m syntax local notation `lift` := @monad_lift basic_parser_m _ _ _ diff --git a/tests/lean/parser1.lean.expected.out b/tests/lean/parser1.lean.expected.out index 5479f1b8c1..e05bb1d273 100644 --- a/tests/lean/parser1.lean.expected.out +++ b/tests/lean/parser1.lean.expected.out @@ -3,7 +3,7 @@ result: result: [(module [] - [(import "import" [(import_path [] (id (ident_part (1 "me")) []))])] + [(import "import" [(import_path [] (ident (ident_part (1 "me")) []))])] []) (eoi "")] error at line 1, column 0: @@ -23,48 +23,48 @@ result: [(prelude "prelude")] [(import "import" - [(import_path ["." "."] (id (ident_part (1 "a")) [])) - (import_path [] (id (ident_part (1 "b")) []))]) - (import "import" [(import_path [] (id (ident_part (1 "c")) []))])] + [(import_path ["." "."] (ident (ident_part (1 "a")) [])) + (import_path [] (ident (ident_part (1 "b")) []))]) + (import "import" [(import_path [] (ident (ident_part (1 "c")) []))])] []) (eoi "")] result: [(module [] [] - [(open + [(command.open "open" - [(open_spec (id (ident_part (1 "me")) []) [] [] [] []) - (open_spec (id (ident_part (1 "you")) []) [] [] [] [])])]) + [(command.open_spec (ident (ident_part (1 "me")) []) [] [] [] []) + (command.open_spec (ident (ident_part (1 "you")) []) [] [] [] [])])]) (eoi "")] result: [(module [] [] - [(open + [(command.open "open" - [(open_spec - (id (ident_part (1 "me")) []) - [(open_spec.as "as" (id (ident_part (1 "you")) []))] - [(open_spec.only - ["(" (id (ident_part (1 "a")) [])] - [(id (ident_part (1 "b")) []) (id (ident_part (1 "c")) [])] + [(command.open_spec + (ident (ident_part (1 "me")) []) + [(command.open_spec.as "as" (ident (ident_part (1 "you")) []))] + [(command.open_spec.only + ["(" (ident (ident_part (1 "a")) [])] + [(ident (ident_part (1 "b")) []) (ident (ident_part (1 "c")) [])] ")")] - [(open_spec.renaming + [(command.open_spec.renaming ["(" "renaming"] - [(open_spec.renaming.item - (id (ident_part (1 "a")) []) + [(command.open_spec.renaming.item + (ident (ident_part (1 "a")) []) "->" - (id (ident_part (1 "b")) [])) - (open_spec.renaming.item - (id (ident_part (1 "c")) []) + (ident (ident_part (1 "b")) [])) + (command.open_spec.renaming.item + (ident (ident_part (1 "c")) []) "->" - (id (ident_part (1 "d")) []))] + (ident (ident_part (1 "d")) []))] ")")] - [(open_spec.hiding + [(command.open_spec.hiding "(" "hiding" - [(id (ident_part (1 "a")) []) (id (ident_part (1 "b")) [])] + [(ident (ident_part (1 "a")) []) (ident (ident_part (1 "b")) [])] ")")])])]) (eoi "")] error at line 1, column 11: @@ -73,10 +73,10 @@ partial syntax tree: [(module [] [] - [(open + [(command.open "open" - [(open_spec (id (ident_part (1 "me")) []) [] [] [] []) - (open_spec (id (ident_part (1 "you")) []) [] [] [] [])])]) + [(command.open_spec (ident (ident_part (1 "me")) []) [] [] [] []) + (command.open_spec (ident (ident_part (1 "you")) []) [] [] [] [])])]) (eoi "")] error at line 1, column 5: expected identifier @@ -86,12 +86,14 @@ partial syntax tree: [(module [] [] - [(open + [(command.open "open" - [(open_spec ) ]) - (open + [(command.open_spec ) + ]) + (command.open "open" - [(open_spec ) ])]) + [(command.open_spec ) + ])]) (eoi "")] error at line 1, column 8: expected command @@ -99,559 +101,619 @@ partial syntax tree: [(module [] [] - [(open "open" [(open_spec (id (ident_part (1 "me")) []) [] [] [] [])]) - (open "open" [(open_spec (id (ident_part (1 "you")) []) [] [] [] [])])]) + [(command.open + "open" + [(command.open_spec (ident (ident_part (1 "me")) []) [] [] [] [])]) + (command.open + "open" + [(command.open_spec (ident (ident_part (1 "you")) []) [] [] [] [])])]) (eoi "")] result: [(module [] [] - [(open "open" [(open_spec (id (ident_part (1 "a")) []) [] [] [] [])]) - (section + [(command.open + "open" + [(command.open_spec (ident (ident_part (1 "a")) []) [] [] [] [])]) + (command.section "section" - [(id (ident_part (1 "b")) [])] - [(open "open" [(open_spec (id (ident_part (1 "c")) []) [] [] [] [])]) - (section + [(ident (ident_part (1 "b")) [])] + [(command.open + "open" + [(command.open_spec (ident (ident_part (1 "c")) []) [] [] [] [])]) + (command.section "section" - [(id (ident_part (1 "d")) [])] - [(open "open" [(open_spec (id (ident_part (1 "e")) []) [] [] [] [])])] + [(ident (ident_part (1 "d")) [])] + [(command.open + "open" + [(command.open_spec (ident (ident_part (1 "e")) []) [] [] [] [])])] "end" - [(id (ident_part (1 "d")) [])])] + [(ident (ident_part (1 "d")) [])])] "end" - [(id (ident_part (1 "b")) [])])]) + [(ident (ident_part (1 "b")) [])])]) (eoi "")] result: -[(module [] [] [(section "section" [(id (ident_part (1 "a")) [])] [] "end" [])]) +[(module + [] + [] + [(command.section "section" [(ident (ident_part (1 "a")) [])] [] "end" [])]) (eoi "")] Type (max u v) : Type ((max u v)+1) result: [(module [] [] - [(check + [(command.check "#check" (term.app (term.app (term.sort_app (term.sort (1 "Type")) - (level.leading (0 (id (ident_part (1 "max")) [])))) - (id (ident_part (1 "u")) [])) - (id (ident_part (1 "v")) [])))]) + (level.leading (0 (ident (ident_part (1 "max")) [])))) + (term.ident (ident (ident_part (1 "u")) []) [])) + (term.ident (ident (ident_part (1 "v")) []) [])))]) (eoi "")] -(notation +(command.notation "notation" - (notation_spec + (command.notation_spec (1 - (notation_spec.rules + (command.notation_spec.rules [] - [(notation_spec.rule - (notation_spec.notation_symbol + [(command.notation_spec.rule + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" "+" "`" - [(notation_spec.precedence ":" (base10_lit "10"))]))) - [(notation_spec.transition + [(command.notation_spec.precedence ":" (base10_lit "10"))]))) + [(command.notation_spec.transition (2 - (notation_spec.argument - (id (ident_part (1 "b")) []) - [(notation_spec.action ":" (notation_spec.action_kind (0 (base10_lit "10"))))])))])]))) + (command.notation_spec.argument + (ident (ident_part (1 "b")) []) + [(command.notation_spec.action + ":" + (command.notation_spec.action_kind (0 (base10_lit "10"))))])))])]))) ":=" (term.hole "_")) notation`+`:10 b:10 :=_ -error at line 85, column 0: -expected command -partial syntax tree: +result: [(module [(prelude "prelude")] [] - [(notation + [(command.notation "notation" - (notation_spec + (command.notation_spec (1 - (notation_spec.rules + (command.notation_spec.rules [] - [(notation_spec.rule - (notation_spec.notation_symbol - (0 (notation_spec.notation_quoted_symbol "`" "Prop" "`" []))) + [(command.notation_spec.rule + (command.notation_spec.notation_symbol + (0 (command.notation_spec.notation_quoted_symbol "`" "Prop" "`" []))) [])]))) ":=" (term.sort_app (term.sort (0 "Sort")) (level.leading (4 (base10_lit "0"))))) - (notation + (command.notation "notation" - (notation_spec + (command.notation_spec (1 - (notation_spec.rules - [(id (ident_part (1 "f")) [])] - [(notation_spec.rule - (notation_spec.notation_symbol + (command.notation_spec.rules + [(ident (ident_part (1 "f")) [])] + [(command.notation_spec.rule + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "$ " + " $ " "`" - [(notation_spec.precedence ":" (base10_lit "1"))]))) - [(notation_spec.transition + [(command.notation_spec.precedence ":" (base10_lit "1"))]))) + [(command.notation_spec.transition (2 - (notation_spec.argument - (id (ident_part (1 "a")) []) - [(notation_spec.action ":" (notation_spec.action_kind (0 (base10_lit "0"))))])))])]))) + (command.notation_spec.argument + (ident (ident_part (1 "a")) []) + [(command.notation_spec.action + ":" + (command.notation_spec.action_kind (0 (base10_lit "0"))))])))])]))) ":=" - (term.app (id (ident_part (1 "f")) []) (id (ident_part (1 "a")) []))) - (reserve_mixfix - ["reserve" (mixfix.kind (0 "prefix"))] - (notation_spec.notation_symbol + (term.app + (term.ident (ident (ident_part (1 "f")) []) []) + (term.ident (ident (ident_part (1 "a")) []) []))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (0 "prefix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" "¬" "`" - [(notation_spec.precedence ":" (base10_lit "40"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (0 "prefix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "40"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (0 "prefix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" "~" "`" - [(notation_spec.precedence ":" (base10_lit "40"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (3 "infixr"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "40"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (3 "infixr"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "∧ " + " ∧ " "`" - [(notation_spec.precedence ":" (base10_lit "35"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (3 "infixr"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "35"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (3 "infixr"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "/\\ " + " /\\ " "`" - [(notation_spec.precedence ":" (base10_lit "35"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (3 "infixr"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "35"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (3 "infixr"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "\\/ " + " \\/ " "`" - [(notation_spec.precedence ":" (base10_lit "30"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (3 "infixr"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "30"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (3 "infixr"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "∨ " + " ∨ " "`" - [(notation_spec.precedence ":" (base10_lit "30"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "30"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "<-> " + " <-> " "`" - [(notation_spec.precedence ":" (base10_lit "20"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "20"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "↔ " + " ↔ " "`" - [(notation_spec.precedence ":" (base10_lit "20"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "20"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "= " + " = " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "== " + " == " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "≠ " + " ≠ " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "≈ " + " ≈ " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "~ " + " ~ " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "≡ " + " ≡ " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (2 "infixl"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (2 "infixl"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "⬝ " + " ⬝ " "`" - [(notation_spec.precedence ":" (base10_lit "75"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (3 "infixr"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "75"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (3 "infixr"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "▸ " + " ▸ " "`" - [(notation_spec.precedence ":" (base10_lit "75"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (3 "infixr"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "75"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (3 "infixr"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "▹ " + " ▹ " "`" - [(notation_spec.precedence ":" (base10_lit "75"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (3 "infixr"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "75"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (3 "infixr"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "⊕ " + " ⊕ " "`" - [(notation_spec.precedence ":" (base10_lit "30"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (3 "infixr"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "30"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (3 "infixr"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "× " + " × " "`" - [(notation_spec.precedence ":" (base10_lit "35"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (2 "infixl"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "35"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (2 "infixl"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "+ " + " + " "`" - [(notation_spec.precedence ":" (base10_lit "65"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (2 "infixl"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "65"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (2 "infixl"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "- " + " - " "`" - [(notation_spec.precedence ":" (base10_lit "65"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (2 "infixl"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "65"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (2 "infixl"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "* " + " * " "`" - [(notation_spec.precedence ":" (base10_lit "70"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (2 "infixl"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "70"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (2 "infixl"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "/ " + " / " "`" - [(notation_spec.precedence ":" (base10_lit "70"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (2 "infixl"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "70"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (2 "infixl"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "% " + " % " "`" - [(notation_spec.precedence ":" (base10_lit "70"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (2 "infixl"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "70"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (2 "infixl"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "%ₙ " + " %ₙ " "`" - [(notation_spec.precedence ":" (base10_lit "70"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (0 "prefix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "70"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (0 "prefix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" "-" "`" - [(notation_spec.precedence ":" (base10_lit "100"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (3 "infixr"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "100"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (3 "infixr"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "^ " + " ^ " "`" - [(notation_spec.precedence ":" (base10_lit "80"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (3 "infixr"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "80"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (3 "infixr"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "∘ " + " ∘ " "`" - [(notation_spec.precedence ":" (base10_lit "90"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "90"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "<= " + " <= " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "≤ " + " ≤ " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "< " + " < " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - ">= " + " >= " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "≥ " + " ≥ " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "> " + " > " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (0 "prefix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (0 "prefix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" "!" "`" - [(notation_spec.precedence ":" (base10_lit "40"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (2 "infixl"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "40"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (2 "infixl"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "&& " + " && " "`" - [(notation_spec.precedence ":" (base10_lit "35"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (2 "infixl"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "35"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (2 "infixl"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "|| " + " || " "`" - [(notation_spec.precedence ":" (base10_lit "30"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "30"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "∈ " + " ∈ " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "∉ " + " ∉ " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (2 "infixl"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (2 "infixl"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "∩ " + " ∩ " "`" - [(notation_spec.precedence ":" (base10_lit "70"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (2 "infixl"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "70"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (2 "infixl"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "∪ " + " ∪ " "`" - [(notation_spec.precedence ":" (base10_lit "65"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "65"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "⊆ " + " ⊆ " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "⊇ " + " ⊇ " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "⊂ " + " ⊂ " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "⊃ " + " ⊃ " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "\\ " + " \\ " "`" - [(notation_spec.precedence ":" (base10_lit "70"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (1 "infix"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "70"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (1 "infix"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "∣ " + " ∣ " "`" - [(notation_spec.precedence ":" (base10_lit "50"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (2 "infixl"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "50"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (2 "infixl"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - "++ " + " ++ " "`" - [(notation_spec.precedence ":" (base10_lit "65"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (3 "infixr"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "65"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (3 "infixr"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" - ":: " + " :: " "`" - [(notation_spec.precedence ":" (base10_lit "67"))])))) - (reserve_mixfix - ["reserve" (mixfix.kind (2 "infixl"))] - (notation_spec.notation_symbol + [(command.notation_spec.precedence ":" (base10_lit "67"))])))) + (command.reserve_mixfix + ["reserve" (command.mixfix.kind (2 "infixl"))] + (command.notation_spec.notation_symbol (0 - (notation_spec.notation_quoted_symbol + (command.notation_spec.notation_quoted_symbol "`" "; " "`" - [(notation_spec.precedence ":" (base10_lit "1"))])))) - (universes + [(command.notation_spec.precedence ":" (base10_lit "1"))])))) + (command.universes "universes" - [(id (ident_part (1 "u")) []) - (id (ident_part (1 "v")) []) - (id (ident_part (1 "w")) [])])]) + [(ident (ident_part (1 "u")) []) + (ident (ident_part (1 "v")) []) + (ident (ident_part (1 "w")) [])]) + (command.declaration + (command.decl_modifiers + [] + [] + [] + [(command.decl_attribute + "@[" + [(command.attr_instance (ident (ident_part (1 "inline")) []) [])] + "]")]) + (command.declaration.inner + (0 + (command.def + "def" + (ident (ident_part (1 "id")) []) + (command.decl_sig + [(term.bracketed_binder + (1 + (term.implicit_binder + "{" + (term.binder_content + [(term.binder_id (0 (term.ident (ident (ident_part (1 "α")) []) [])))] + (term.binder_content_type + ":" + (term.sort_app + (term.sort (0 "Sort")) + (level.leading (5 (ident (ident_part (1 "u")) []))))) + []) + "}"))) + (term.bracketed_binder + (0 + (term.explicit_binder + "(" + (term.explicit_binder_content + (1 + (term.binder_content + [(term.binder_id (0 (term.ident (ident (ident_part (1 "a")) []) [])))] + (term.binder_content_type ":" (term.ident (ident (ident_part (1 "α")) []) [])) + []))) + ")")))] + [(command.decl_type ":" (term.ident (ident (ident_part (1 "α")) []) []))]) + (command.decl_val + (0 + (command.simple_decl_val ":=" (term.ident (ident (ident_part (1 "a")) []) []))))))))]) (eoi "")]