From 945bf39e0536fd7142db7e7ea6a76b2d7d750ad7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 28 Sep 2018 20:49:59 -0700 Subject: [PATCH] feat(library/init/lean): progress --- library/init/core.lean | 18 +- library/init/lean/elaborator.lean | 40 + library/init/lean/expander.lean | 8 +- library/init/lean/parser/command.lean | 36 +- library/init/lean/parser/declaration.lean | 11 +- library/init/lean/parser/notation.lean | 46 +- library/init/lean/parser/term.lean | 123 +- library/init/lean/parser/token.lean | 6 +- tests/lean/parser1.lean | 11 +- tests/lean/parser1.lean.expected.out | 2612 +-------------------- 10 files changed, 281 insertions(+), 2630 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index 22772e3611..a9ee8e9999 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -328,7 +328,7 @@ inductive list (T : Type u) | nil {} : list | cons (hd : T) (tl : list) : list -notation h :: t := list.cons h t +infixr :: := list.cons notation `[` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) := l inductive nat @@ -375,7 +375,7 @@ export has_andthen (andthen) export has_pow (pow) infix ∈ := has_mem.mem -notation a ∉ s := ¬ has_mem.mem a s +notation a ` ∉ ` s := ¬ has_mem.mem a s infix + := has_add.add infix * := has_mul.mul infix - := has_sub.sub @@ -471,7 +471,7 @@ be stronger than application. def std.prec.max_plus : nat := std.prec.max + 10 -notation α × β := prod α β +infixr × := prod -- notation for n-ary tuples /- sizeof -/ @@ -618,9 +618,9 @@ attribute [elab_simple] bin_tree.node bin_tree.leaf | ff tt := tt | _ _ := ff -notation !x := bnot x -notation x || y := bor x y -notation x && y := band x y +prefix ! := bnot +infix || := bor +infix && := band /- Logical connectives an equality -/ @@ -687,7 +687,7 @@ theorem cast_proof_irrel {α β : Sort u} (h₁ h₂ : α = β) (a : α) : cast theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a := rfl @[reducible] def ne {α : Sort u} (a b : α) := ¬(a = b) -notation a ≠ b := ne a b +infix ≠ := ne theorem ne.def {α : Sort u} (a b : α) : a ≠ b = ¬ (a = b) := rfl @@ -1530,10 +1530,10 @@ variables {α : Type u} {β : Type v} variable f : α → α → α variable inv : α → α variable one : α -local notation a * b := f a b +local infix * := f local postfix `⁻¹`:max := inv variable g : α → α → α -local notation a + b := g a b +local infix + := g def commutative := ∀ a b, a * b = b * a def associative := ∀ a b c, (a * b) * c = a * (b * c) diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index d4061ef4b5..4f86022d90 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -33,6 +33,46 @@ do cfg ← read, local attribute [instance] name.has_lt_quick +def prec_to_nat (prec : option precedence.view) : nat := +(prec <&> λ p, p.prec.to_nat).get_or_else 0 + +def command_parser_config.register_notation_tokens (spec : notation_spec.view) (cfg : command_parser_config) : + except string command_parser_config := +do spec.rules.mfoldl (λ (cfg : command_parser_config) r, match r.symbol with + | notation_symbol.view.quoted {symbol := syntax.atom a, prec := prec, ..} := + pure {cfg with tokens := cfg.tokens.insert a.val.trim {«prefix» := a.val.trim, lbp := prec_to_nat prec}} + | _ := throw "register_notation_tokens: unreachable") cfg + +def command_parser_config.register_notation_parser (spec : notation_spec.view) (cfg : command_parser_config) : + except string command_parser_config := +do -- build and register parser + let k : syntax_node_kind := {name := "notation"}, + ps ← spec.rules.mmap (λ r : rule.view, do + psym ← match r.symbol with + | notation_symbol.view.quoted {symbol := syntax.atom a ..} := + pure (symbol a.val : term_parser) + | _ := throw "register_notation_parser: unreachable", + ptrans ← match r.transition with + | some (transition.view.binders b) := + pure $ some $ term.binders.parser + | some (transition.view.arg {action := none, ..}) := + pure $ some term.parser + | some (transition.view.arg {action := some {action := action_kind.view.prec prec}, ..}) := + pure $ some $ term.parser prec.to_nat + | some (transition.view.arg {action := some {action := action_kind.view.scoped sc}, ..}) := + pure $ some $ term.parser $ prec_to_nat sc.prec + | none := pure $ none + | _ := throw "register_notation_parser: unimplemented", + pure $ psym::ptrans.to_monad + ), + let ps := ps.bind id, + cfg ← match spec.prefix_arg with + | none := pure {cfg with leading_term_parsers := + parser.combinators.node k ps::cfg.leading_term_parsers} + | some _ := pure {cfg with trailing_term_parsers := + parser.combinators.node k (read::ps.map coe)::cfg.trailing_term_parsers}, + pure cfg + def postprocess_notation_spec (spec : notation_spec.view) : notation_spec.view := -- default leading tokens to `max` -- NOTE: should happen after copying precedences from reserved notation diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean index 067e8f58e7..b080b605a5 100644 --- a/library/init/lean/expander.lean +++ b/library/init/lean/expander.lean @@ -37,11 +37,11 @@ instance coe_name_ident : has_coe name parser.ident.view := instance coe_ident_term_ident : has_coe parser.ident.view term.ident.view := ⟨λ id, {id := id}⟩ -instance coe_term_ident_binder_id : has_coe term.ident.view binder_id.view := -⟨binder_id.view.id⟩ +instance coe_term_ident_binder_id : has_coe term.ident.view binder_ident.view := +⟨binder_ident.view.id⟩ -instance coe_binders {α : Type} [has_coe_t α binder_id.view] : has_coe (list α) term.binders.view := -⟨λ ids, binders.view.unbracketed {ids := ids.map coe}⟩ +instance coe_binders {α : Type} [has_coe_t α binder_ident.view] : has_coe (list α) term.binders.view := +⟨λ ids, {leading_ids := ids.map coe}⟩ def mixfix_to_notation_spec (k : mixfix.kind.view) (sym : notation_symbol.view) : transform_m notation_spec.view := let prec := match sym with diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean index b77d45f013..eb9d7e8e0f 100644 --- a/library/init/lean/parser/command.lean +++ b/library/init/lean/parser/command.lean @@ -40,9 +40,29 @@ node! open_spec [ def open.parser : command_parser := node! «open» ["open", spec: open_spec.parser] +@[derive parser.has_tokens] +def export.parser : command_parser := +node! «export» ["export", spec: open_spec.parser] + @[derive parser.has_tokens] def section.parser : command_parser := -node! «section» ["section", name: ident.parser?, commands: command.parser*, "end", end_name: ident.parser?] +node! «section» ["section", name: ident.parser?] + +@[derive parser.has_tokens] +def namespace.parser : command_parser := +node! «namespace» ["namespace", name: ident.parser] + +@[derive parser.has_tokens] +def variable.parser : command_parser := +node! «variable» ["variable", binder: term.bracketed_binder.parser] + +@[derive parser.has_tokens] +def variables.parser : command_parser := +node! «variables» ["variables", binders: term.bracketed_binder.parser+] + +@[derive parser.has_tokens] +def end.parser : command_parser := +node! «end» ["end", name: ident.parser?] @[derive parser.has_tokens] def universe.parser : command_parser := @@ -58,10 +78,22 @@ any_of [ def check.parser : command_parser := node! check ["#check", term: term.parser] +@[derive parser.has_tokens parser.has_view] +def attribute.parser : command_parser := +node! «attribute» [ + «local»: (symbol "local ")?, + "attribute ", + "[", + attrs: sep_by1 attr_instance.parser (symbol ", "), + "] ", + ids: ident.parser* +] + @[derive has_tokens] def builtin_command_parsers : list command_parser := [ open.parser, section.parser, universe.parser, notation.parser, reserve_notation.parser, - mixfix.parser, reserve_mixfix.parser, check.parser, declaration.parser] + mixfix.parser, reserve_mixfix.parser, check.parser, declaration.parser, attribute.parser, + export.parser, namespace.parser, end.parser, variable.parser, variables.parser] end «command» def command_parser.run (commands : list command_parser) (p : command_parser) diff --git a/library/init/lean/parser/declaration.lean b/library/init/lean/parser/declaration.lean index 00fff8bae1..9b3252901c 100644 --- a/library/init/lean/parser/declaration.lean +++ b/library/init/lean/parser/declaration.lean @@ -40,7 +40,7 @@ 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 +-- TODO(Sebastian): custom attribute parsers node! decl_attribute ["@[", attrs: sep_by1 attr_instance.parser (symbol ","), "]"] set_option class.instance_max_depth 300 @@ -115,17 +115,18 @@ def declaration.parser : command_parser := node! declaration [ modifiers: decl_modifiers.parser, inner: node_choice! declaration.inner { - «def»: node! «def» ["def", + «def_like»: node! «def_like» [ + kind: node_choice! def_like.kind {"def", "abbreviation", "theorem"}, old_univ_params: node! old_univ_params ["{", ids: ident.parser+, "}"]?, name: term.ident.parser, sig: decl_sig.parser, val: decl_val.parser], - «abbreviation»: node! «abbreviation» ["abbreviation", name: term.ident.parser, sig: decl_sig.parser, val: decl_val.parser], - «theorem»: node! «theorem» ["theorem", name: term.ident.parser, sig: decl_sig.parser, val: decl_val.parser], «instance»: node! «instance» ["instance", name: term.ident.parser?, sig: decl_sig.parser, val: decl_val.parser], «example»: node! «example» ["example", sig: decl_sig.parser, val: decl_val.parser], «constant»: node! «constant» ["constant", name: term.ident.parser, sig: decl_sig.parser], «axiom»: node! «axiom» ["axiom", name: term.ident.parser, sig: decl_sig.parser], - «inductive»: node! «inductive» ["inductive", name: term.ident.parser, sig: decl_sig.parser, + «inductive»: node! «inductive» [try [«class»: (symbol "class")?, "inductive"], + name: term.ident.parser, + sig: decl_sig.parser, local_notation: notation_like.parser?, intro_rules: intro_rule.parser*], «structure»: structure.parser, diff --git a/library/init/lean/parser/notation.lean b/library/init/lean/parser/notation.lean index 8c67f13e43..85ad10c76b 100644 --- a/library/init/lean/parser/notation.lean +++ b/library/init/lean/parser/notation.lean @@ -77,7 +77,15 @@ node! action [":", action: node_choice! action_kind { prec: number.parser, max: symbol_or_ident "max", prev: symbol_or_ident "prev", - scoped: symbol_or_ident "scoped" + scoped: node! scoped_action [ + "(", + scoped: symbol_or_ident "scoped", + prec: precedence.parser?, + id: ident.parser, + ", ", + term: term.parser, + ")", + ], /-TODO seq [ "(", any_of ["foldl", "foldr"], @@ -87,8 +95,8 @@ node! action [":", action: node_choice! action_kind { @[derive parser.has_tokens parser.has_view] def transition.parser : term_parser := node_choice! transition { - binder: node! binder ["binder", prec: precedence.parser?], - binders: node! binders ["binders", prec: precedence.parser?], + binder: node! binder [binder: symbol_or_ident "binder", prec: precedence.parser?], + binders: node! binders [binders: symbol_or_ident "binders", prec: precedence.parser?], arg: node! argument [id: ident.parser, action: action.parser?] } @@ -131,37 +139,5 @@ node! «reserve_mixfix» [ symbol: notation_spec.notation_symbol.parser] end «command» -open «command» -open command.notation_spec - -def command_parser_config.register_notation_tokens (spec : notation_spec.view) (cfg : command_parser_config) : - except string command_parser_config := -do spec.rules.mfoldl (λ (cfg : command_parser_config) r, match r.symbol with - | notation_symbol.view.quoted {symbol := syntax.atom a, prec := some prec, ..} := - pure {cfg with tokens := cfg.tokens.insert a.val.trim {«prefix» := a.val.trim, lbp := prec.prec.to_nat}} - | _ := throw "register_notation: unreachable") cfg - -def command_parser_config.register_notation_parser (spec : notation_spec.view) (cfg : command_parser_config) : - except string command_parser_config := -do -- build and register parser - let k : syntax_node_kind := {name := "notation"}, - ps ← spec.rules.mmap (λ r : rule.view, do - psym ← match r.symbol with - | notation_symbol.view.quoted {symbol := syntax.atom a ..} := - pure (symbol a.val : term_parser) - | _ := throw "register_notation: unreachable", - ptrans ← match r.transition with - | some (transition.view.arg {action := some {action := action_kind.view.prec prec}, ..}) := - pure $ some $ term.parser prec.to_nat - | none := pure $ none - | _ := throw "register_notation: unimplemented", - pure $ psym::ptrans.to_monad - ), - let ps := ps.bind id, - cfg ← match spec.prefix_arg with - | none := pure {cfg with leading_term_parsers := node k ps::cfg.leading_term_parsers} - | some _ := pure {cfg with trailing_term_parsers := node k (read::ps.map coe)::cfg.trailing_term_parsers}, - pure cfg - end parser end lean diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index 18f29a1cbe..6d2b867874 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -34,9 +34,18 @@ instance : has_view get_leading syntax := default _ @[derive parser.has_tokens parser.has_view] def paren.parser : term_parser := -/- Do not allow trailing comma. Looks a bit weird and would clash with - adding support for tuple sections (https://downloads.haskell.org/~ghc/8.2.1/docs/html/users_guide/glasgow_exts.html#tuple-sections). -/ -node! «paren» ["(":max_prec, elems: sep_by (term.parser 0) (symbol ",") ff, ")"] +node! «paren» ["(":max_prec, + content: node! paren_content [ + term: term.parser, + special: node_choice! paren_special { + /- Do not allow trailing comma. Looks a bit weird and would clash with + adding support for tuple sections (https://downloads.haskell.org/~ghc/8.2.1/docs/html/users_guide/glasgow_exts.html#tuple-sections). -/ + tuple: node! tuple [", ", tail: sep_by (term.parser 0) (symbol ", ") ff], + typed: node! typed [" : ", type: term.parser], + }?, + ]?, + ")" +] @[derive parser.has_tokens parser.has_view] def hole.parser : term_parser := @@ -47,10 +56,14 @@ def sort.parser : term_parser := node_choice! sort {"Sort":max_prec, "Type":max_prec} section binder +@[derive has_tokens has_view] +def binder_ident.parser : term_parser := +node_choice! binder_ident {id: ident.parser, hole: hole.parser} + @[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})+, + ids: binder_ident.parser+, type: node! binder_content_type [":", type: term.parser 0]?, default: node_choice! binder_default { val: node! binder_default_val [":=", term: term.parser 0], @@ -58,6 +71,10 @@ node! binder_content [ }? ] +@[derive parser.has_tokens parser.has_view] +def anonymous_constructor.parser : term_parser := +node! anonymous_constructor ["⟨":max_prec, args: sep_by (term.parser 0) (symbol ","), "⟩"] + /- 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: @@ -98,17 +115,25 @@ node_choice! bracketed_binder { right: unicode_symbol "⦄" "}}", ], inst_implicit: node! inst_implicit_binder ["[":max_prec, content: longest_match [ - node! inst_implicit_named_binder [id: ident.parser, type: term.parser 0], + node! inst_implicit_named_binder [id: ident.parser, " : ", type: term.parser 0], node! inst_implicit_anonymous_binder [type: term.parser 0] - ], "]"] + ], "]"], + anonymous_constructor: anonymous_constructor.parser, } @[derive has_tokens has_view] def binders.parser : term_parser := -node_choice! binders { - bracketed: bracketed_binder.parser+, - unbracketed: binder_content.parser, -} +node! binders [ + leading_ids: binder_ident.parser*, + remainder: node_choice! binders_remainder { + type: node! binders_types [":", type: term.parser 0], + -- we allow mixing like in `a (b : β) c`, but not `a : α (b : β) c : γ` + mixed: node_choice! mixed_binder { + bracketed: bracketed_binder.parser, + id: ident.parser, + }+, + }? +] end binder @@ -121,19 +146,27 @@ node! lambda [ body: term.parser 0 ] +@[derive parser.has_tokens parser.has_view] +def assume.parser : term_parser := +node! «assume» [ + "assume ":max_prec, + binders: node_choice! assume_binders { + anonymous: node! assume_anonymous [": ", type: term.parser], + binders: binders.parser + }, + ", ", + body: term.parser 0 +] + @[derive parser.has_tokens parser.has_view] def pi.parser : term_parser := node! pi [ - op: unicode_symbol "Π" "Pi" max_prec, + op: any_of [unicode_symbol "Π" "Pi" max_prec, unicode_symbol "∀" "forall" max_prec], binders: binders.parser, ",", range: term.parser 0 ] -@[derive parser.has_tokens parser.has_view] -def anonymous_constructor.parser : term_parser := -node! anonymous_constructor ["⟨":max_prec, args: sep_by (term.parser 0) (symbol ","), "⟩"] - @[derive parser.has_tokens parser.has_view] def explicit_ident.parser : term_parser := node! explicit [ @@ -144,6 +177,59 @@ node! explicit [ id: term.ident.parser ] +@[derive parser.has_tokens parser.has_view] +def from.parser : term_parser := +node! «from» ["from ", proof: term.parser] + +@[derive parser.has_tokens parser.has_view] +def have.parser : term_parser := +node! «have» [ + "have ", + id: (try node! have_id [id: ident.parser, " : "])?, + prop: term.parser, + proof: node_choice! have_proof { + term: node! have_term [" := ", term: term.parser], + «from»: node! have_from [", ", «from»: from.parser], + }, + ", ", + body: term.parser, +] + +@[derive parser.has_tokens parser.has_view] +def show.parser : term_parser := +node! «show» [ + "show ", + prop: term.parser, + ", ", + «from»: from.parser, +] + +@[derive parser.has_tokens parser.has_view] +def match.parser : term_parser := +node! «match» [ + "match ", + scrutinees: sep_by1 term.parser (symbol ", ") ff, + type: node! match_type [" : ", type: term.parser]?, + " with ", + opt_bar: (symbol " | ")?, + equations: sep_by1 + node! «match_equation» [ + lhs: sep_by1 term.parser (symbol ", ") ff, ":=", rhs: term.parser] + (symbol " | ") ff, +] + +@[derive parser.has_tokens parser.has_view] +def if.parser : term_parser := +node! «if» [ + "if ", + id: (try node! if_id [id: ident.parser, " : "])?, + prop: term.parser, + " then ", + then_branch: term.parser, + " else ", + else_branch: term.parser, +] + -- TODO(Sebastian): replace with attribute @[derive has_tokens] def builtin_leading_parsers : list term_parser := [ @@ -155,7 +241,12 @@ def builtin_leading_parsers : list term_parser := [ lambda.parser, pi.parser, anonymous_constructor.parser, - explicit_ident.parser + explicit_ident.parser, + have.parser, + show.parser, + assume.parser, + match.parser, + if.parser ] @[derive parser.has_tokens parser.has_view] diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean index 363db934b1..dee4d42d7d 100644 --- a/library/init/lean/parser/token.lean +++ b/library/init/lean/parser/token.lean @@ -40,7 +40,7 @@ do r ← remaining, private def whitespace_aux : nat → basic_parser_m unit | (n+1) := do whitespace, - str "--" *> take_while' (= '\n') *> whitespace_aux n <|> + str "--" *> take_while' (≠ '\n') *> whitespace_aux n <|> -- a "/--" doc comment is an actual token, not whitespace try (str "/-" *> not_followed_by (str "-")) *> finish_comment_block *> whitespace_aux n <|> pure () @@ -181,14 +181,14 @@ lift $ try $ do { } repr sym instance symbol.tokens (sym lbp) : parser.has_tokens (symbol sym lbp : parser) := -⟨[⟨sym, lbp, none⟩]⟩ +⟨[⟨sym.trim, lbp, none⟩]⟩ instance symbol.view (sym lbp) : parser.has_view (symbol sym lbp : parser) (option syntax_atom) := { view := λ stx, match stx with | syntax.atom atom := some atom | _ := none, review := λ a, (syntax.atom <$> a).get_or_else syntax.missing } instance symbol.view_default (sym lbp) : parser.has_view_default (symbol sym lbp : parser) _ - (some {info := none, val := sym}) := ⟨⟩ + (some {info := none, val := sym.trim}) := ⟨⟩ def number.parser : parser := lift $ try $ do { diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean index 14ec6e23a5..2487b9e7aa 100644 --- a/tests/lean/parser1.lean +++ b/tests/lean/parser1.lean @@ -87,9 +87,10 @@ universes u v pure cmd'.reprint -- slowly progressing... +--set_option profiler true #eval (do { s ← io.fs.read_file "../../library/init/core.lean", - let s := (s.mk_iterator.nextn 7000).prev_to_string, + let s := (s.mk_iterator.nextn 50000).prev_to_string, parser_cfg ← monad_except.lift_except $ mk_config, let cfg : elaborator_config := {filename := "foo"}, let st : elaborator_state := {parser_cfg := {..parser_cfg}}, @@ -112,13 +113,13 @@ universes u v --io.println cmd', match ((elaborate cmd').run cfg).run st with | except.ok ((), st) := pure (sum.inl (k, st, out :: outs)) - | except.error e := throw e.text + | except.error e := io.println e.text *> pure (sum.inl (k, st, out :: outs)) } - | except.error e := throw e.text + | except.error e := io.println e.text *> pure (sum.inl (k, st, out :: outs)) }, - check_reprint outs s, + check_reprint outs s/-, let stx := syntax.node ⟨none, outs.map (λ r, r.cmd)⟩, let stx := stx.update_leading s, io.println "result:", - io.println (to_string stx) + io.println (to_string stx)-/ } : except_t string io unit) diff --git a/tests/lean/parser1.lean.expected.out b/tests/lean/parser1.lean.expected.out index 0e27ed701c..67d49f5f29 100644 --- a/tests/lean/parser1.lean.expected.out +++ b/tests/lean/parser1.lean.expected.out @@ -79,21 +79,18 @@ partial syntax tree: result: [(module.header [] []) (command.open "open" [(command.open_spec `a [] [] [] [])]) - (command.section - "section" - [`b] - [(command.open "open" [(command.open_spec `c [] [] [] [])]) - (command.section - "section" - [`d] - [(command.open "open" [(command.open_spec `e [] [] [] [])])] - "end" - [`d])] - "end" - [`b]) + (command.section "section" [`b]) + (command.open "open" [(command.open_spec `c [] [] [] [])]) + (command.section "section" [`d]) + (command.open "open" [(command.open_spec `e [] [] [] [])]) + (command.end "end" [`d]) + (command.end "end" [`b]) (eoi "")] result: -[(module.header [] []) (command.section "section" [`a] [] "end" []) (eoi "")] +[(module.header [] []) + (command.section "section" [`a]) + (command.end "end" []) + (eoi "")] Type (max u v) : Type ((max u v)+1) result: [(module.header [] []) @@ -106,2541 +103,54 @@ result: (term.ident `v []))) (eoi "")] (ok "notationa`+`:65 b:65 :=nat.addab") -error at line 242, column 5: -expected command -result: -[(module.header [(module.prelude "prelude")] []) - (command.notation - "notation" - (command.notation_spec - [] - [(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 (number (0 "0")))))) - (command.notation - "notation" - (command.notation_spec - [`f] - [(command.notation_spec.rule - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " $ " - "`" - [(command.notation_spec.precedence ":" (number (0 "1")))]))) - [(command.notation_spec.transition - (2 - (command.notation_spec.argument - `a - [(command.notation_spec.action - ":" - (command.notation_spec.action_kind (0 (number (0 "0")))))])))])]) - ":=" - (term.app (term.ident `f []) (term.ident `a []))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (0 "prefix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - "¬" - "`" - [(command.notation_spec.precedence ":" (number (0 "40")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (0 "prefix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - "~" - "`" - [(command.notation_spec.precedence ":" (number (0 "40")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (3 "infixr"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ∧ " - "`" - [(command.notation_spec.precedence ":" (number (0 "35")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (3 "infixr"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " /\\ " - "`" - [(command.notation_spec.precedence ":" (number (0 "35")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (3 "infixr"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " \\/ " - "`" - [(command.notation_spec.precedence ":" (number (0 "30")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (3 "infixr"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ∨ " - "`" - [(command.notation_spec.precedence ":" (number (0 "30")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " <-> " - "`" - [(command.notation_spec.precedence ":" (number (0 "20")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ↔ " - "`" - [(command.notation_spec.precedence ":" (number (0 "20")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " = " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " == " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ≠ " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ≈ " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ~ " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ≡ " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (2 "infixl"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ⬝ " - "`" - [(command.notation_spec.precedence ":" (number (0 "75")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (3 "infixr"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ▸ " - "`" - [(command.notation_spec.precedence ":" (number (0 "75")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (3 "infixr"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ▹ " - "`" - [(command.notation_spec.precedence ":" (number (0 "75")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (3 "infixr"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ⊕ " - "`" - [(command.notation_spec.precedence ":" (number (0 "30")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (3 "infixr"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " × " - "`" - [(command.notation_spec.precedence ":" (number (0 "35")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (2 "infixl"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " + " - "`" - [(command.notation_spec.precedence ":" (number (0 "65")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (2 "infixl"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " - " - "`" - [(command.notation_spec.precedence ":" (number (0 "65")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (2 "infixl"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " * " - "`" - [(command.notation_spec.precedence ":" (number (0 "70")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (2 "infixl"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " / " - "`" - [(command.notation_spec.precedence ":" (number (0 "70")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (2 "infixl"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " % " - "`" - [(command.notation_spec.precedence ":" (number (0 "70")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (2 "infixl"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " %ₙ " - "`" - [(command.notation_spec.precedence ":" (number (0 "70")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (0 "prefix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - "-" - "`" - [(command.notation_spec.precedence ":" (number (0 "100")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (3 "infixr"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ^ " - "`" - [(command.notation_spec.precedence ":" (number (0 "80")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (3 "infixr"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ∘ " - "`" - [(command.notation_spec.precedence ":" (number (0 "90")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " <= " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ≤ " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " < " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " >= " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ≥ " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " > " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (0 "prefix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - "!" - "`" - [(command.notation_spec.precedence ":" (number (0 "40")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (2 "infixl"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " && " - "`" - [(command.notation_spec.precedence ":" (number (0 "35")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (2 "infixl"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " || " - "`" - [(command.notation_spec.precedence ":" (number (0 "30")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ∈ " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ∉ " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (2 "infixl"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ∩ " - "`" - [(command.notation_spec.precedence ":" (number (0 "70")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (2 "infixl"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ∪ " - "`" - [(command.notation_spec.precedence ":" (number (0 "65")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ⊆ " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ⊇ " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ⊂ " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ⊃ " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " \\ " - "`" - [(command.notation_spec.precedence ":" (number (0 "70")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (1 "infix"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ∣ " - "`" - [(command.notation_spec.precedence ":" (number (0 "50")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (2 "infixl"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " ++ " - "`" - [(command.notation_spec.precedence ":" (number (0 "65")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (3 "infixr"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - " :: " - "`" - [(command.notation_spec.precedence ":" (number (0 "67")))])))) - (command.reserve_mixfix - ["reserve" (command.mixfix.kind (2 "infixl"))] - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - "; " - "`" - [(command.notation_spec.precedence ":" (number (0 "1")))])))) - (command.universes "universes" [`u `v `w]) - (command.declaration - (command.decl_modifiers - ["/-- Auxiliary meta constant used by the compiler when erasing proofs from code. -/"] - [] - [] - ["meta"] - []) - (command.declaration.inner - (5 - (command.constant - "constant" - (term.ident `lc_proof []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type ":" (notation "Prop"))] - []) - "}")))] - [(command.decl_type ":" (term.ident `α []))]))))) - (command.declaration - (command.decl_modifiers - ["/-- Auxiliary meta constant used by the compiler to mark unreachable code. -/"] - [] - [] - ["meta"] - []) - (command.declaration.inner - (5 - (command.constant - "constant" - (term.ident `lc_unreachable []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}")))] - [(command.decl_type ":" (term.ident `α []))]))))) - (command.declaration - (command.decl_modifiers - ["/-- Auxiliary meta constant used by the compiler to mark type casting. -/"] - [] - [] - ["meta"] - []) - (command.declaration.inner - (5 - (command.constant - "constant" - (term.ident `lc_cast []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `β [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `v))))] - []) - "}")))] - [(command.decl_type ":" (term.arrow (term.ident `α []) "→" (term.ident `β [])))]))))) - (command.declaration - (command.decl_modifiers - [] - [] - [] - [] - [(command.decl_attribute "@[" [(command.attr_instance `inline [])] "]")]) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `id []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `a [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []))) - ")")))] - [(command.decl_type ":" (term.ident `α []))]) - (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `a [])))))))) - (command.declaration - (command.decl_modifiers - [] - [] - [] - [] - [(command.decl_attribute "@[" [(command.attr_instance `inline [])] "]")]) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `flip []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `β [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `v))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `φ [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `w))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `f [])))] - [(term.binder_content_type - ":" - (term.arrow - (term.ident `α []) - "→" - (term.arrow (term.ident `β []) "→" (term.ident `φ []))))] - []))) - ")")))] - [(command.decl_type - ":" - (term.arrow - (term.ident `β []) - "→" - (term.arrow (term.ident `α []) "→" (term.ident `φ []))))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.lambda - "λ" - (term.binders - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `b []))) - (term.binder_id (0 (term.ident `a [])))] - [] - []))) - "," - (term.app (term.app (term.ident `f []) (term.ident `a [])) (term.ident `b [])))))))))) - (command.declaration - (command.decl_modifiers - [] - [] - [] - [] - [(command.decl_attribute "@[" [(command.attr_instance `inline [])] "]")]) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `id_delta []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `a [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []))) - ")")))] - [(command.decl_type ":" (term.ident `α []))]) - (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `a [])))))))) - (command.declaration - (command.decl_modifiers - ["/-- Gadget for optional parameter support. -/"] - [] - [] - [] - [(command.decl_attribute "@[" [(command.attr_instance `reducible [])] "]")]) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `opt_param []) - (command.decl_sig - [(term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []))) - ")"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `default [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []))) - ")")))] - [(command.decl_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]) - (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `α [])))))))) - (command.declaration - (command.decl_modifiers - ["/-- Gadget for marking output parameters in type classes. -/"] - [] - [] - [] - [(command.decl_attribute "@[" [(command.attr_instance `reducible [])] "]")]) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `out_param []) - (command.decl_sig - [(term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []))) - ")")))] - [(command.decl_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]) - (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `α [])))))))) - (command.declaration - (command.decl_modifiers - ["/-- Auxiliary declaration used to implement the notation (a : α) -/"] - [] - [] - [] - [(command.decl_attribute "@[" [(command.attr_instance `reducible [])] "]")]) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `typed_expr []) - (command.decl_sig - [(term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []))) - ")"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `a [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []))) - ")")))] - [(command.decl_type ":" (term.ident `α []))]) - (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `a [])))))))) - (command.declaration - (command.decl_modifiers - [] - [] - [] - [] - [(command.decl_attribute "@[" [(command.attr_instance `macro_inline [])] "]")]) - (command.declaration.inner - (1 - (command.abbreviation - "abbreviation" - (term.ident `id_rhs []) - (command.decl_sig - [(term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []))) - ")"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `a [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []))) - ")")))] - [(command.decl_type ":" (term.ident `α []))]) - (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `a [])))))))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (7 - (command.inductive - "inductive" - (term.ident `punit []) - (command.decl_sig - [] - [(command.decl_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]) - [] - [(command.intro_rule - "|" - `star - [] - (command.decl_sig [] [(command.decl_type ":" (term.ident `punit []))]))])))) - (command.declaration - (command.decl_modifiers - ["/-- An abbreviation for `punit.{0}`, its most common instantiation.\n This type should be preferred over `punit` where possible to avoid\n unnecessary universe parameters. -/"] - [] - [] - [] - []) - (command.declaration.inner - (1 - (command.abbreviation - "abbreviation" - (term.ident `unit []) - (command.decl_sig [] [(command.decl_type ":" (term.sort (1 "Type")))]) - (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `punit [])))))))) - (command.declaration - (command.decl_modifiers - [] - [] - [] - [] - [(command.decl_attribute "@[" [(command.attr_instance `pattern [])] "]")]) - (command.declaration.inner - (1 - (command.abbreviation - "abbreviation" - (term.ident `unit.star []) - (command.decl_sig [] [(command.decl_type ":" (term.ident `unit []))]) - (command.decl_val - (0 (command.simple_decl_val ":=" (term.ident `punit.star [])))))))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (8 - (command.structure - "structure" - (term.ident `thunk []) - (command.decl_sig - [(term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))] - []))) - ")")))] - [(command.decl_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))]) - [] - ":=" - [] - [(command.structure_field - (1 - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `fn [])))] - [(term.binder_content_type - ":" - (term.arrow (term.ident `unit []) "→" (term.ident `α [])))] - []))) - ")")))))])))) - (command.declaration - (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] []) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `thunk.pure []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `a [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []))) - ")")))] - [(command.decl_type ":" (term.app (term.ident `thunk []) (term.ident `α [])))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.anonymous_constructor - "⟨" - [(term.lambda - "λ" - (term.binders - (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] []))) - "," - (term.ident `a []))] - "⟩")))))))) - (command.declaration - (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] []) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `thunk.get []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `x [])))] - [(term.binder_content_type - ":" - (term.app (term.ident `thunk []) (term.ident `α [])))] - []))) - ")")))] - [(command.decl_type ":" (term.ident `α []))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.app (term.ident `x.fn []) (term.paren "(" [] ")"))))))))) - (command.declaration - (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] []) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `thunk.map []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `β [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `v))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `f [])))] - [(term.binder_content_type - ":" - (term.arrow (term.ident `α []) "→" (term.ident `β [])))] - []))) - ")"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `x [])))] - [(term.binder_content_type - ":" - (term.app (term.ident `thunk []) (term.ident `α [])))] - []))) - ")")))] - [(command.decl_type ":" (term.app (term.ident `thunk []) (term.ident `β [])))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.anonymous_constructor - "⟨" - [(term.lambda - "λ" - (term.binders - (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] []))) - "," - (term.app (term.ident `f []) (term.ident `x.get [])))] - "⟩")))))))) - (command.declaration - (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] []) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `thunk.bind []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `β [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `v))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `x [])))] - [(term.binder_content_type - ":" - (term.app (term.ident `thunk []) (term.ident `α [])))] - []))) - ")"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `f [])))] - [(term.binder_content_type - ":" - (term.arrow - (term.ident `α []) - "→" - (term.app (term.ident `thunk []) (term.ident `β []))))] - []))) - ")")))] - [(command.decl_type ":" (term.app (term.ident `thunk []) (term.ident `β [])))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.anonymous_constructor - "⟨" - [(term.lambda - "λ" - (term.binders - (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] []))) - "," - (term.projection - (term.paren "(" [(term.app (term.ident `f []) (term.ident `x.get []))] ")") - "." - (term.projection_spec (0 `get))))] - "⟩")))))))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (8 - (command.structure - "structure" - (term.ident `task []) - (command.decl_sig - [(term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))] - []))) - ")")))] - [(command.decl_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))]) - [] - ":=" - [] - [(command.structure_field - (1 - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `fn [])))] - [(term.binder_content_type - ":" - (term.arrow (term.ident `unit []) "→" (term.ident `α [])))] - []))) - ")")))))])))) - (command.declaration - (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] []) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `task.pure []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `a [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []))) - ")")))] - [(command.decl_type ":" (term.app (term.ident `task []) (term.ident `α [])))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.anonymous_constructor - "⟨" - [(term.lambda - "λ" - (term.binders - (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] []))) - "," - (term.ident `a []))] - "⟩")))))))) - (command.declaration - (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] []) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `task.get []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `x [])))] - [(term.binder_content_type - ":" - (term.app (term.ident `task []) (term.ident `α [])))] - []))) - ")")))] - [(command.decl_type ":" (term.ident `α []))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.app (term.ident `x.fn []) (term.paren "(" [] ")"))))))))) - (command.declaration - (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] []) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `task.map []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `β [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `v))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `f [])))] - [(term.binder_content_type - ":" - (term.arrow (term.ident `α []) "→" (term.ident `β [])))] - []))) - ")"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `x [])))] - [(term.binder_content_type - ":" - (term.app (term.ident `task []) (term.ident `α [])))] - []))) - ")")))] - [(command.decl_type ":" (term.app (term.ident `task []) (term.ident `β [])))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.anonymous_constructor - "⟨" - [(term.lambda - "λ" - (term.binders - (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] []))) - "," - (term.app (term.ident `f []) (term.ident `x.get [])))] - "⟩")))))))) - (command.declaration - (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] []) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `task.bind []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `β [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `v))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `x [])))] - [(term.binder_content_type - ":" - (term.app (term.ident `task []) (term.ident `α [])))] - []))) - ")"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `f [])))] - [(term.binder_content_type - ":" - (term.arrow - (term.ident `α []) - "→" - (term.app (term.ident `task []) (term.ident `β []))))] - []))) - ")")))] - [(command.decl_type ":" (term.app (term.ident `task []) (term.ident `β [])))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.anonymous_constructor - "⟨" - [(term.lambda - "λ" - (term.binders - (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] []))) - "," - (term.projection - (term.paren "(" [(term.app (term.ident `f []) (term.ident `x.get []))] ")") - "." - (term.projection_spec (0 `get))))] - "⟩")))))))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (7 - (command.inductive - "inductive" - (term.ident `true []) - (command.decl_sig [] [(command.decl_type ":" (notation "Prop"))]) - [] - [(command.intro_rule - "|" - `intro - [] - (command.decl_sig [] [(command.decl_type ":" (term.ident `true []))]))])))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (7 - (command.inductive - "inductive" - (term.ident `false []) - (command.decl_sig [] [(command.decl_type ":" (notation "Prop"))]) - [] - [])))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (7 - (command.inductive - "inductive" - (term.ident `empty []) - (command.decl_sig [] [(command.decl_type ":" (term.sort (1 "Type")))]) - [] - [])))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `not []) - (command.decl_sig - [(term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `a [])))] - [(term.binder_content_type ":" (notation "Prop"))] - []))) - ")")))] - [(command.decl_type ":" (notation "Prop"))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.arrow (term.ident `a []) "→" (term.ident `false []))))))))) - (command.mixfix - (command.mixfix.kind (0 "prefix")) - (command.notation_spec.mixfix_symbol - (0 (command.notation_spec.notation_quoted_symbol "`" "¬" "`" []))) - ":=" - (term.ident `not [])) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (7 - (command.inductive - "inductive" - (term.ident `eq []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `a [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []))) - ")")))] - [(command.decl_type - ":" - (term.arrow (term.ident `α []) "→" (notation "Prop")))]) - [] - [(command.intro_rule - "|" - `refl - [] - (command.decl_sig - [] - [(command.decl_type ":" (term.app (term.ident `eq []) (term.ident `a [])))]))])))) - (command.declaration - (command.decl_modifiers - [] - [] - [] - [] - [(command.decl_attribute - "@[" - [(command.attr_instance `elab_as_eliminator []) - "," - (command.attr_instance `inline []) - "," - (command.attr_instance `reducible [])] - "]")]) - (command.declaration.inner - (0 - (command.def - "def" - [(command.old_univ_params "{" [`u1 `u2] "}")] - (term.ident `eq.ndrec []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u2))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `a [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `C [])))] - [(term.binder_content_type - ":" - (term.arrow - (term.ident `α []) - "→" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u1)))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `m [])))] - [(term.binder_content_type ":" (term.app (term.ident `C []) (term.ident `a [])))] - []))) - ")"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `b [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `h [])))] - [(term.binder_content_type - ":" - (term.app (term.app (term.ident `eq []) (term.ident `a [])) (term.ident `b [])))] - []))) - ")")))] - [(command.decl_type ":" (term.app (term.ident `C []) (term.ident `b [])))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.app - (term.app - (term.app - (term.app - (term.app - (term.app - (term.explicit (term.explicit_modifier (0 "@")) (term.ident `eq.rec [])) - (term.ident `α [])) - (term.ident `a [])) - (term.paren - "(" - [(term.lambda - "λ" - (term.binders - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `α []))) (term.binder_id (1 (term.hole "_")))] - [] - []))) - "," - (term.app (term.ident `C []) (term.ident `α [])))] - ")")) - (term.ident `m [])) - (term.ident `b [])) - (term.ident `h []))))))))) - (command.declaration - (command.decl_modifiers - [] - [] - [] - [] - [(command.decl_attribute - "@[" - [(command.attr_instance `elab_as_eliminator []) - "," - (command.attr_instance `inline []) - "," - (command.attr_instance `reducible [])] - "]")]) - (command.declaration.inner - (0 - (command.def - "def" - [(command.old_univ_params "{" [`u1 `u2] "}")] - (term.ident `eq.ndrec_on []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u2))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `a [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `C [])))] - [(term.binder_content_type - ":" - (term.arrow - (term.ident `α []) - "→" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u1)))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `b [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `h [])))] - [(term.binder_content_type - ":" - (term.app (term.app (term.ident `eq []) (term.ident `a [])) (term.ident `b [])))] - []))) - ")"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `m [])))] - [(term.binder_content_type ":" (term.app (term.ident `C []) (term.ident `a [])))] - []))) - ")")))] - [(command.decl_type ":" (term.app (term.ident `C []) (term.ident `b [])))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.app - (term.app - (term.app - (term.app - (term.app - (term.app - (term.app - (term.explicit (term.explicit_modifier (0 "@")) (term.ident `eq.rec [])) - (term.ident `α [])) - (term.ident `a [])) - (term.paren - "(" - [(term.lambda - "λ" - (term.binders - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `α []))) (term.binder_id (1 (term.hole "_")))] - [] - []))) - "," - (term.app (term.ident `C []) (term.ident `α [])))] - ")")) - (term.ident `m [])) - (term.ident `b [])) - (term.ident `h [])) - (term.ident `init_quot []))))))))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (7 - (command.inductive - "inductive" - (term.ident `heq []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `a [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []))) - ")")))] - [(command.decl_type - ":" - (term.pi - "Π" - (term.binders - (0 - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `β [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}")))])) - "," - (term.arrow (term.ident `β []) "→" (notation "Prop"))))]) - [] - [(command.intro_rule - "|" - `refl - [] - (command.decl_sig - [] - [(command.decl_type ":" (term.app (term.ident `heq []) (term.ident `a [])))]))])))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (8 - (command.structure - "structure" - (term.ident `prod []) - (command.decl_sig - [(term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))] - []))) - ")"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `β [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (1 "Type")) (level.leading (5 `v))))] - []))) - ")")))] - []) - [] - ":=" - [] - [(command.structure_field - (1 - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `fst [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []))) - ")"))))) - (command.structure_field - (1 - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `snd [])))] - [(term.binder_content_type ":" (term.ident `β []))] - []))) - ")")))))])))) - (command.declaration - (command.decl_modifiers - ["/-- Similar to `prod`, but α and β can be propositions.\n We use this type internally to automatically generate the brec_on recursor. -/"] - [] - [] - [] - []) - (command.declaration.inner - (8 - (command.structure - "structure" - (term.ident `pprod []) - (command.decl_sig - [(term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []))) - ")"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `β [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `v))))] - []))) - ")")))] - []) - [] - ":=" - [] - [(command.structure_field - (1 - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `fst [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []))) - ")"))))) - (command.structure_field - (1 - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `snd [])))] - [(term.binder_content_type ":" (term.ident `β []))] - []))) - ")")))))])))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (8 - (command.structure - "structure" - (term.ident `and []) - (command.decl_sig - [(term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `a []))) - (term.binder_id (0 (term.ident `b [])))] - [(term.binder_content_type ":" (notation "Prop"))] - []))) - ")")))] - [(command.decl_type ":" (notation "Prop"))]) - [] - ":=" - [(command.structure_ctor `intro [] "::")] - [(command.structure_field - (1 - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `left [])))] - [(term.binder_content_type ":" (term.ident `a []))] - []))) - ")"))))) - (command.structure_field - (1 - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `right [])))] - [(term.binder_content_type ":" (term.ident `b []))] - []))) - ")")))))])))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `and.elim_left []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `a []))) - (term.binder_id (0 (term.ident `b [])))] - [(term.binder_content_type ":" (notation "Prop"))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `h [])))] - [(term.binder_content_type - ":" - (term.app (term.app (term.ident `and []) (term.ident `a [])) (term.ident `b [])))] - []))) - ")")))] - [(command.decl_type ":" (term.ident `a []))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.projection - (term.ident `h []) - "." - (term.projection_spec (1 (number (0 "1")))))))))))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `and.elim_right []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `a []))) - (term.binder_id (0 (term.ident `b [])))] - [(term.binder_content_type ":" (notation "Prop"))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `h [])))] - [(term.binder_content_type - ":" - (term.app (term.app (term.ident `and []) (term.ident `a [])) (term.ident `b [])))] - []))) - ")")))] - [(command.decl_type ":" (term.ident `b []))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.projection - (term.ident `h []) - "." - (term.projection_spec (1 (number (0 "2")))))))))))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (8 - (command.structure - "structure" - (term.ident `iff []) - (command.decl_sig - [(term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `a []))) - (term.binder_id (0 (term.ident `b [])))] - [(term.binder_content_type ":" (notation "Prop"))] - []))) - ")")))] - [(command.decl_type ":" (notation "Prop"))]) - [] - ":=" - [(command.structure_ctor `intro [] "::")] - [(command.structure_field - (1 - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `mp [])))] - [(term.binder_content_type - ":" - (term.arrow (term.ident `a []) "→" (term.ident `b [])))] - []))) - ")"))))) - (command.structure_field - (1 - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `mpr [])))] - [(term.binder_content_type - ":" - (term.arrow (term.ident `b []) "→" (term.ident `a [])))] - []))) - ")")))))])))) - (command.mixfix - (command.mixfix.kind (1 "infix")) - (command.notation_spec.mixfix_symbol (1 "=")) - ":=" - (term.ident `eq [])) - (command.declaration - (command.decl_modifiers - [] - [] - [] - [] - [(command.decl_attribute "@[" [(command.attr_instance `pattern [])] "]")]) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `rfl []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `a [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []) - "}")))] - [(command.decl_type - ":" - (notation (term.ident `a []) "=" (term.ident `a [])))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.app (term.ident `eq.refl []) (term.ident `a []))))))))) - (command.declaration - (command.decl_modifiers - [] - [] - [] - [] - [(command.decl_attribute - "@[" - [(command.attr_instance `elab_as_eliminator [])] - "]")]) - (command.declaration.inner - (2 - (command.theorem - "theorem" - (term.ident `eq.subst []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `P [])))] - [(term.binder_content_type - ":" - (term.arrow (term.ident `α []) "→" (notation "Prop")))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `a []))) - (term.binder_id (0 (term.ident `b [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `h₁ [])))] - [(term.binder_content_type - ":" - (notation (term.ident `a []) "=" (term.ident `b [])))] - []))) - ")"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `h₂ [])))] - [(term.binder_content_type ":" (term.app (term.ident `P []) (term.ident `a [])))] - []))) - ")")))] - [(command.decl_type ":" (term.app (term.ident `P []) (term.ident `b [])))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.app - (term.app (term.ident `eq.ndrec []) (term.ident `h₂ [])) - (term.ident `h₁ []))))))))) - (command.mixfix - (command.mixfix.kind (3 "infixr")) - (command.notation_spec.mixfix_symbol (1 "▸")) - ":=" - (term.ident `eq.subst [])) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (2 - (command.theorem - "theorem" - (term.ident `eq.trans []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `a []))) - (term.binder_id (0 (term.ident `b []))) - (term.binder_id (0 (term.ident `c [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `h₁ [])))] - [(term.binder_content_type - ":" - (notation (term.ident `a []) "=" (term.ident `b [])))] - []))) - ")"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `h₂ [])))] - [(term.binder_content_type - ":" - (notation (term.ident `b []) "=" (term.ident `c [])))] - []))) - ")")))] - [(command.decl_type - ":" - (notation (term.ident `a []) "=" (term.ident `c [])))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (notation (term.ident `h₂ []) "▸" (term.ident `h₁ []))))))))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (2 - (command.theorem - "theorem" - (term.ident `eq.symm []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `a []))) - (term.binder_id (0 (term.ident `b [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `h [])))] - [(term.binder_content_type - ":" - (notation (term.ident `a []) "=" (term.ident `b [])))] - []))) - ")")))] - [(command.decl_type - ":" - (notation (term.ident `b []) "=" (term.ident `a [])))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (notation (term.ident `h []) "▸" (term.ident `rfl []))))))))) - (command.mixfix - (command.mixfix.kind (1 "infix")) - (command.notation_spec.mixfix_symbol (1 "==")) - ":=" - (term.ident `heq [])) - (command.declaration - (command.decl_modifiers - [] - [] - [] - [] - [(command.decl_attribute "@[" [(command.attr_instance `pattern [])] "]")]) - (command.declaration.inner - (0 - (command.def - "def" - [] - (term.ident `heq.rfl []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `a [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []) - "}")))] - [(command.decl_type - ":" - (notation (term.ident `a []) "==" (term.ident `a [])))]) - (command.decl_val - (0 - (command.simple_decl_val - ":=" - (term.app (term.ident `heq.refl []) (term.ident `a []))))))))) - (command.declaration - (command.decl_modifiers [] [] [] [] []) - (command.declaration.inner - (2 - (command.theorem - "theorem" - (term.ident `eq_of_heq []) - (command.decl_sig - [(term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `α [])))] - [(term.binder_content_type - ":" - (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))] - []) - "}"))) - (term.bracketed_binder - (1 - (term.implicit_binder - "{" - (term.binder_content - [(term.binder_id (0 (term.ident `a []))) - (term.binder_id (0 (term.ident `a' [])))] - [(term.binder_content_type ":" (term.ident `α []))] - []) - "}"))) - (term.bracketed_binder - (0 - (term.explicit_binder - "(" - (term.explicit_binder_content - (1 - (term.binder_content - [(term.binder_id (0 (term.ident `h [])))] - [(term.binder_content_type - ":" - (notation (term.ident `a []) "==" (term.ident `a' [])))] - []))) - ")")))] - [(command.decl_type - ":" - (notation (term.ident `a []) "=" (term.ident `a' [])))]) - (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `have [])))))))) - (eoi "")] +error at line 332, column 16: +expected "scoped" +register_notation_tokens: unreachable +error at line 1228, column 0: +expected identifier or number +error at line 1232, column 0: +unexpected token "{" +expected term +error at line 1239, column 0: +unexpected token "{" +expected term +error at line 1361, column 10: +expected identifier +error at line 1458, column 40: +unexpected token ":=" +expected ")" +error at line 1462, column 41: +unexpected token ":=" +expected ")" +error at line 1466, column 50: +unexpected token ":=" +expected ")" +error at line 1470, column 55: +unexpected token ":=" +expected ")" +error at line 1475, column 6: +unexpected token "infix" +expected "attribute" +error at line 1530, column 9: +expected "(", "{", "⦃", "{{", "[" or "⟨" +error at line 1531, column 9: +expected "(", "{", "⦃", "{{", "[" or "⟨" +error at line 1532, column 9: +expected "(", "{", "⦃", "{{", "[" or "⟨" +error at line 1533, column 6: +unexpected token "infix" +expected "attribute" +error at line 1534, column 6: +unexpected token "postfix" +expected "attribute" +error at line 1534, column 19: +expected number +register_notation_tokens: unreachable +error at line 1535, column 9: +expected "(", "{", "⦃", "{{", "[" or "⟨" +error at line 1536, column 6: +unexpected token "infix" +expected "attribute" +error at line 1542, column 18: +unexpected end of file +expected "(", "{", "⦃", "{{", "[", "⟨", ":", ":=", "." or "|"