diff --git a/stage0/src/Lean/Elab/Quotation.lean b/stage0/src/Lean/Elab/Quotation.lean
index e61890af2f..99fc9d708c 100644
--- a/stage0/src/Lean/Elab/Quotation.lean
+++ b/stage0/src/Lean/Elab/Quotation.lean
@@ -124,7 +124,9 @@ def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do
 
 @[builtinTermElab Parser.Level.quot] def elabLevelQuot : TermElab := adaptExpander stxQuot.expand
 @[builtinTermElab Parser.Term.quot] def elabTermQuot : TermElab := adaptExpander stxQuot.expand
-@[builtinTermElab Parser.Term.funBinder.quot] def elabfunBinderQuot : TermElab := adaptExpander stxQuot.expand
+@[builtinTermElab Parser.Term.funBinder.quot] def elabFunBinderQuot : TermElab := adaptExpander stxQuot.expand
+@[builtinTermElab Parser.Term.bracketedBinder.quot] def elabBracketedBinderQuot : TermElab := adaptExpander stxQuot.expand
+@[builtinTermElab Parser.Term.matchDiscr.quot] def elabMatchDiscrQuot : TermElab := adaptExpander stxQuot.expand
 @[builtinTermElab Parser.Tactic.quot] def elabTacticQuot : TermElab := adaptExpander stxQuot.expand
 @[builtinTermElab Parser.Tactic.quotSeq] def elabTacticQuotSeq : TermElab := adaptExpander stxQuot.expand
 @[builtinTermElab Parser.Term.stx.quot] def elabStxQuot : TermElab := adaptExpander stxQuot.expand
diff --git a/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 1e75bac785..3d71f1b4be 100644
--- a/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -219,7 +219,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation do
     Syntax.mkApp stx st.moreArgs
   | _,        #[] => failure
   | _,        _   =>
-    let discrs ← st.discrs.mapM fun discr => `(matchDiscr|$discr:term)
+    let discrs ← st.discrs.mapM fun discr => `(Parser.Term.matchDiscr|$discr:term)
     let pats ← delabPatterns st
     let stx ← `(match $[$discrs],* with | $[$[$pats],* => $st.rhss]|*)
     Syntax.mkApp stx st.moreArgs
diff --git a/stage0/stdlib/Lean/Elab/Quotation.c b/stage0/stdlib/Lean/Elab/Quotation.c
index 69263b3e57..48b2faa4b5 100644
--- a/stage0/stdlib/Lean/Elab/Quotation.c
+++ b/stage0/stdlib/Lean/Elab/Quotation.c
@@ -180,7 +180,6 @@ lean_object* l_Lean_Syntax_getAntiquotTerm(lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_12545____closed__6;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__9___closed__7;
 lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___spec__8___closed__4;
-lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__2;
 lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___closed__31;
 lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_Quotation_match__syntax_expand___spec__3(size_t, size_t, lean_object*);
 lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__1;
@@ -228,6 +227,7 @@ lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lea
 extern lean_object* l_Lean_Format_sbracket___closed__2;
 lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__18;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_12545____closed__13;
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__1;
 lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__5;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_49____closed__5;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__23;
@@ -235,6 +235,7 @@ lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compile
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_floatOutAntiquotTerms(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_zip___rarg(lean_object*, lean_object*);
 lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___lambda__2___closed__10;
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot(lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_5703____closed__3;
 lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabLevelQuot___closed__1;
 lean_object* l_Lean_Elab_Term_Quotation_mkTuple___closed__5;
@@ -256,6 +257,7 @@ extern lean_object* l___private_Init_Meta_0__Lean_quoteOption___rarg___closed__6
 lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabLevelQuot___closed__2;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_8703____closed__7;
 lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___spec__12___closed__2;
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__2;
 lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuotSeq(lean_object*);
 lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___spec__12(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_instQuoteBool___closed__5;
@@ -270,7 +272,7 @@ lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSy
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__9___closed__14;
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
-lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot(lean_object*);
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot___closed__2;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_floatOutAntiquotTerms___lambda__1___boxed__const__1;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_10790____closed__15;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_12545____closed__2;
@@ -279,6 +281,7 @@ lean_object* l_Lean_Elab_Term_Quotation_instInhabitedHeadInfo___closed__3;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_10790____closed__10;
 extern lean_object* l_Lean_numLitKind;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot___closed__1;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_11154____closed__4;
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__9___closed__31;
@@ -353,6 +356,7 @@ lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__3;
 lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuotSeq___closed__3;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__34;
 extern lean_object* l_Lean_instInhabitedSourceInfo___closed__1;
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__3;
 lean_object* l_Lean_Elab_Term_Quotation_match__syntax_expand_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___spec__13(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__13;
@@ -382,9 +386,10 @@ lean_object* l_Lean_Elab_Term_Quotation_instInhabitedHeadInfo___closed__1;
 lean_object* l_Lean_Elab_Term_Quotation_getAntiquotationIds(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_bind___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_command__Unif__hint______Where___x7c_x2d_u22a2_____closed__11;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__1___closed__2;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_letBindRhss___closed__11;
-lean_object* l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_9845_(lean_object*);
+lean_object* l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_9853_(lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__3;
 lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -418,6 +423,7 @@ lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compile
 extern lean_object* l_Lean_nullKind___closed__1;
 uint8_t l_Lean_Syntax_isAntiquot(lean_object*);
 lean_object* l_Lean_addTrace___at_Lean_Elab_Term_Quotation_match__syntax_expand___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot(lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__56;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__9___closed__40;
@@ -458,7 +464,6 @@ extern lean_object* l_Lean_myMacro____x40_Init_Notation___hyg_12778____closed__3
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__1___closed__2;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch_match__3(lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot(lean_object*);
-lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__4;
 lean_object* l___private_Init_Meta_0__Lean_quoteList___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__3(lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__9___closed__8;
 extern lean_object* l_Lean_instToMessageDataOption___rarg___closed__3;
@@ -483,6 +488,7 @@ lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compile
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__15;
 lean_object* l_Lean_Elab_Term_Quotation_mkTuple___closed__6;
 lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___closed__3;
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot(lean_object*);
 lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__9___closed__27;
 lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__7;
@@ -507,7 +513,6 @@ lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSy
 extern lean_object* l_Lean_Expr_setPPExplicit___closed__3;
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 lean_object* l_List_head_x21___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___spec__2___boxed(lean_object*);
-lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__1;
 lean_object* l_Lean_Elab_Term_Quotation_match__syntax_expand___lambda__3___closed__1;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__9___closed__4;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__42;
@@ -521,12 +526,14 @@ lean_object* l_Lean_Syntax_getArgs(lean_object*);
 lean_object* l_Lean_Elab_Term_Quotation_match__syntax_expand___lambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getAntiquotSpliceSuffix(lean_object*);
 lean_object* l_Lean_Syntax_getKind(lean_object*);
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__1;
 lean_object* l_Lean_Elab_Term_Quotation_BasicHeadInfo_rhsFn___default(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__34;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_explodeHeadPat(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__9___closed__28;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__9___closed__5;
 lean_object* l_List_filterAux___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___spec__6___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_Quotation_elabFunBinderQuot(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___closed__42;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__33;
@@ -540,13 +547,13 @@ lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lea
 extern lean_object* l_Lean_instQuoteSubstring___closed__4;
 lean_object* l_Lean_Elab_Term_Quotation_elabTacticQuotSeq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_head_x21___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___spec__2___closed__1;
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__2;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__54;
 extern lean_object* l_Lean_Format_paren___closed__2;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo(lean_object*);
 lean_object* l_List_head_x21___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__1___boxed(lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___closed__1;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_158____closed__1;
-lean_object* l_Lean_Elab_Term_Quotation_elabfunBinderQuot(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabTermQuot___closed__2;
 lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__3(lean_object*, size_t, size_t, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__2___closed__19;
@@ -560,6 +567,7 @@ lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSy
 extern lean_object* l_List_head_x21___rarg___closed__3;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_Quotation_elabMatchDiscrQuot(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_adaptExpander(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__28;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___closed__3;
@@ -647,6 +655,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_9474____closed__9;
 extern lean_object* l_Lean_List_format___rarg___closed__3;
 lean_object* l_Lean_Syntax_getAntiquotScopeContents(lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getSepFromSplice___boxed(lean_object*);
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__3;
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__6;
 lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___closed__33;
@@ -662,6 +671,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_521____closed__1;
 extern lean_object* l_Lean_Meta_mkPure___rarg___closed__4;
 lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___spec__11___closed__1;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_floatOutAntiquotTerms_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_Quotation_elabBracketedBinderQuot(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_filterAux___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___spec__4___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___lambda__2___closed__9;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_376____closed__7;
@@ -676,7 +686,6 @@ lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean
 lean_object* l_Lean_Elab_Term_Quotation_mkTuple___closed__7;
 lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___spec__8___boxed(lean_object**);
-lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__3;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__2___closed__14;
 lean_object* l_List_lengthAux___rarg(lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_11918____closed__13;
@@ -748,6 +757,7 @@ lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lea
 lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___closed__21;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_letBindRhss___closed__4;
 lean_object* l_List_foldl___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___spec__3___boxed(lean_object*, lean_object*);
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__4;
 lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabDynamicQuot___closed__1;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch_match__5(lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__43;
@@ -10031,7 +10041,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
-lean_object* l_Lean_Elab_Term_Quotation_elabfunBinderQuot(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+lean_object* l_Lean_Elab_Term_Quotation_elabFunBinderQuot(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
 _start:
 {
 lean_object* x_10; lean_object* x_11; 
@@ -10040,7 +10050,7 @@ x_11 = l_Lean_Elab_Term_adaptExpander(x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x
 return x_11;
 }
 }
-static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__1() {
+static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -10048,41 +10058,127 @@ x_1 = lean_mk_string("funBinder");
 return x_1;
 }
 }
-static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__2() {
+static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_myMacro____x40_Init_Notation___hyg_1625____closed__2;
-x_2 = l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__1;
+x_2 = l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__3() {
+static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__2;
+x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__2;
 x_2 = l_Lean_Syntax_isQuot_match__1___rarg___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__4() {
+static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__4() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Quotation_elabfunBinderQuot), 9, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Quotation_elabFunBinderQuot), 9, 0);
 return x_1;
 }
 }
-lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot(lean_object* x_1) {
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_Elab_Term_termElabAttribute;
-x_3 = l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__3;
-x_4 = l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__4;
+x_3 = l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__3;
+x_4 = l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__4;
+x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
+lean_object* l_Lean_Elab_Term_Quotation_elabBracketedBinderQuot(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+_start:
+{
+lean_object* x_10; lean_object* x_11; 
+x_10 = l_Lean_Elab_Term_Quotation_elabLevelQuot___closed__1;
+x_11 = l_Lean_Elab_Term_adaptExpander(x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
+return x_11;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_myMacro____x40_Init_Notation___hyg_1625____closed__2;
+x_2 = l_Lean_command__Unif__hint______Where___x7c_x2d_u22a2_____closed__11;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__1;
+x_2 = l_Lean_Syntax_isQuot_match__1___rarg___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__3() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Quotation_elabBracketedBinderQuot), 9, 0);
+return x_1;
+}
+}
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Elab_Term_termElabAttribute;
+x_3 = l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__2;
+x_4 = l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__3;
+x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
+lean_object* l_Lean_Elab_Term_Quotation_elabMatchDiscrQuot(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+_start:
+{
+lean_object* x_10; lean_object* x_11; 
+x_10 = l_Lean_Elab_Term_Quotation_elabLevelQuot___closed__1;
+x_11 = l_Lean_Elab_Term_adaptExpander(x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
+return x_11;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___closed__14;
+x_2 = l_Lean_Syntax_isQuot_match__1___rarg___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot___closed__2() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Quotation_elabMatchDiscrQuot), 9, 0);
+return x_1;
+}
+}
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Elab_Term_termElabAttribute;
+x_3 = l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot___closed__1;
+x_4 = l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot___closed__2;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
@@ -13236,7 +13332,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getSepFromSplice___closed__2;
 x_2 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_explodeHeadPat___closed__1;
-x_3 = lean_unsigned_to_nat(241u);
+x_3 = lean_unsigned_to_nat(243u);
 x_4 = lean_unsigned_to_nat(9u);
 x_5 = l_Lean_Syntax_strLitToAtom___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -23302,7 +23398,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getSepFromSplice___closed__2;
 x_2 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___closed__4;
-x_3 = lean_unsigned_to_nat(312u);
+x_3 = lean_unsigned_to_nat(314u);
 x_4 = lean_unsigned_to_nat(12u);
 x_5 = l_Lean_Syntax_strLitToAtom___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -28103,7 +28199,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
-lean_object* l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_9845_(lean_object* x_1) {
+lean_object* l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_9853_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
@@ -28484,15 +28580,31 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabTermQuot___clos
 res = l___regBuiltin_Lean_Elab_Term_Quotation_elabTermQuot(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__1();
-lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__1);
-l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__2();
-lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__2);
-l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__3 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__3();
-lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__3);
-l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__4 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__4();
-lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__4);
-res = l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot(lean_io_mk_world());
+l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__1();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__1);
+l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__2();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__2);
+l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__3 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__3();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__3);
+l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__4 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__4();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot___closed__4);
+res = l___regBuiltin_Lean_Elab_Term_Quotation_elabFunBinderQuot(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__1();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__1);
+l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__2();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__2);
+l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__3 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__3();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot___closed__3);
+res = l___regBuiltin_Lean_Elab_Term_Quotation_elabBracketedBinderQuot(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot___closed__1();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot___closed__1);
+l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot___closed__2();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot___closed__2);
+res = l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchDiscrQuot(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuot___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuot___closed__1();
@@ -28839,7 +28951,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSyntax___c
 res = l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSyntax(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_9845_(lean_io_mk_world());
+res = l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_9853_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));