chore: update stage0

2020-01-17 17:36:17 -08:00 · 2020-01-17 17:36:17 -08:00 · eda70a5567
commit eda70a5567
parent 0caa11e242
13 changed files with 6313 additions and 6281 deletions
--- a/stage0/src/Init/Lean/Elab/BuiltinNotation.lean
+++ b/stage0/src/Init/Lean/Elab/BuiltinNotation.lean
@ -13,8 +13,9 @@ namespace Term

@[builtinTermElab dollar] def elabDollar : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
-| `($f $ $a) => `($f $a)
-| _          => throwUnsupportedSyntax
+| `($f $args* $ $a) => let args := args.push a; `($f $args*)
+| `($f $ $a)        => `($f $a)
+| _                 => throwUnsupportedSyntax

@[builtinTermElab dollarProj] def elabDollarProj : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
--- a/stage0/src/Init/Lean/Elab/Term.lean
+++ b/stage0/src/Init/Lean/Elab/Term.lean
@ -355,17 +355,10 @@ let instIdx := s.instImplicitIdx;
 modify $ fun s => { instImplicitIdx := s.instImplicitIdx + 1, .. s};
 pure $ (`_inst).appendIndexAfter instIdx

-/--
-  Return true if the given syntax is a `Lean.Parser.Term.cdot` or
-  is a `Lean.Parser.Term.app` containing a `cdot`.
-  We use this function as a filter to skip `expandCDotAux` (the expensive part)
-  at `expandCDot?` -/
-private partial def hasCDot : Syntax → Bool
-| stx =>
-  match_syntax stx with
-  | `(·)     => true
-  | `($f $a) => hasCDot f || hasCDot a
-  | _        => false
+private partial def isCDot (stx : Syntax) : Bool :=
+match_syntax stx with
+| `(·) => true
+| _    => false

 /--
  Auxiliary function for expandind the `·` notation.
@ -381,37 +374,29 @@ withFreshMacroScope $
     pure id
  | _ => pure stx

-/--
-  Auxiliary function for expanding `·`s occurring as arguments of
-  applications (i.e., `Lean.Parser.Term.app` nodes).
-  Example: `foo · s` should expand into `foo _a_<idx> s` where
-  `_a_<idx>` is a fresh identifier. -/
-private partial def expandCDotInApp : Syntax → StateT (Array Syntax) TermElabM Syntax
-| n =>
-  match_syntax n with
-  | `($f $a) => do f ← expandCDotInApp f; a ← expandCDot a; `($f $a)
-  | n        => pure n
-
 /--
  Return `some` if succeeded expanding `·` notation occurring in
  the given syntax. Otherwise, return `none`.
  Examples:
  - `· + 1` => `fun _a_1 => _a_1 + 1`
  - `f · · b` => `fun _a_1 _a_2 => f _a_1 _a_2 b` -/
-def expandCDot? : Syntax → TermElabM (Option Syntax)
-| n@(Syntax.node k args) =>
-  if args.any hasCDot then
-    if k == `Lean.Parser.Term.app then do
-      (newNode, binders) ← (expandCDotInApp n).run #[];
-      `(fun $binders* => $newNode)
-    else do {
+def expandCDot? (stx : Syntax) : TermElabM (Option Syntax) :=
+match_syntax stx with
+| `($f $args*) =>
+   if args.any isCDot then do
+     (args, binders) ← (args.mapM expandCDot).run #[];
+     `(fun $binders* => $f $args*)
+   else
+     pure none
+| _ => match stx with
+  | Syntax.node k args =>
+    if args.any isCDot then do
      (args, binders) ← (args.mapM expandCDot).run #[];
      let newNode := Syntax.node k args;
      `(fun $binders* => $newNode)
-    }
-  else
-    pure none
-| _ => pure none
+    else
+      pure none
+  | _ => pure none

 private def exceptionToSorry (ref : Syntax) (errMsg : Message) (expectedType? : Option Expr) : TermElabM Expr := do
 expectedType : Expr ← match expectedType? with
--- a/stage0/src/Init/Lean/Elab/TermApp.lean
+++ b/stage0/src/Init/Lean/Elab/TermApp.lean
@ -381,17 +381,21 @@ else
  else
    mergeFailures candidates f

-private partial def expandApp : Syntax → TermElabM (Syntax × Array NamedArg × Array Arg)
-| stx => match_syntax stx with
-  | `($fn ($id := $arg)) => do
-    (stx, namedArgs, args) ← expandApp fn;
-    namedArgs ← addNamedArg id namedArgs { name := id.getId, val := Arg.stx arg };
-    pure (stx, namedArgs, args)
-  | `($fn $arg)       => do
-    (stx, namedArgs, args) ← expandApp fn;
-    let args := args.push $ Arg.stx arg;
-    pure (stx, namedArgs, args)
-  | _                 => pure (stx, #[], #[])
+private partial def expandApp (stx : Syntax) : TermElabM (Syntax × Array NamedArg × Array Arg) := do
+let f    := stx.getArg 0;
+(namedArgs, args) ← (stx.getArg 1).getArgs.foldlM
+  (fun (acc : Array NamedArg × Array Arg) (stx : Syntax) => do
+    let (namedArgs, args) := acc;
+    if stx.getKind == `Lean.Parser.Term.namedArgument then do
+      -- tparser! try ("(" >> ident >> " := ") >> termParser >> ")"
+      let name := (stx.getArg 1).getId;
+      let val  := stx.getArg 3;
+      namedArgs ← addNamedArg stx namedArgs { name := name, val := Arg.stx val };
+      pure (namedArgs, args)
+    else
+      pure (namedArgs, args.push $ Arg.stx stx))
+  (#[], #[]);
+pure (f, namedArgs, args)

@[builtinTermElab app] def elabApp : TermElab :=
 fun stx expectedType? => do
@ -405,11 +409,14 @@ fun stx expectedType? =>
  let args := args.map Arg.stx;
  elabAppAux stx f #[] args expectedType?

-@[builtinTermElab «id»] def elabId : TermElab := elabApp
-@[builtinTermElab explicit] def elabExplicit : TermElab := elabApp
-@[builtinTermElab choice] def elabChoice : TermElab := elabApp
-@[builtinTermElab proj] def elabProj : TermElab := elabApp
-@[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabApp
+def elabAtom : TermElab :=
+fun stx expectedType? => elabAppAux stx stx #[] #[] expectedType?
+
+@[builtinTermElab «id»] def elabId : TermElab := elabAtom
+@[builtinTermElab explicit] def elabExplicit : TermElab := elabAtom
+@[builtinTermElab choice] def elabChoice : TermElab := elabAtom
+@[builtinTermElab proj] def elabProj : TermElab := elabAtom
+@[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabAtom

@[builtinTermElab sortApp] def elabSortApp : TermElab :=
 fun stx _ => do
--- a/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
+++ b/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
--- a/stage0/stdlib/Init/Lean/Elab/Command.c
+++ b/stage0/stdlib/Init/Lean/Elab/Command.c
@ -80,6 +80,7 @@ lean_object* l_Lean_Elab_Command_commandElabAttribute;
 lean_object* l_Lean_Elab_Command_elabUniverse(lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fswap(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_withNamespace___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern uint8_t l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 lean_object* l_Lean_Elab_Command_runTermElabM___rarg___closed__1;
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSetOption___closed__2;
 lean_object* l_Lean_Elab_Command_elabCheck___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -443,7 +444,6 @@ lean_object* l_Lean_Elab_Command_withNamespace___rarg(lean_object*, lean_object*
 lean_object* lean_io_ref_reset(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_compileDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_logUnknownDecl___closed__1;
-extern lean_object* l___private_Init_Lean_Elab_Term_9__elabTermUsing___main___closed__3;
 lean_object* l_Lean_Syntax_getPos(lean_object*);
 lean_object* l_Lean_Elab_Command_State_inhabited;
 lean_object* l_Lean_Elab_Command_elabOpenHiding___boxed(lean_object*, lean_object*, lean_object*);
@ -543,9 +543,9 @@ lean_object* l_Lean_mkConst(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Command_7__mkTermState(lean_object*);
 lean_object* l_Lean_Elab_Command_commandElabAttribute___closed__5;
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabNamespace___closed__1;
-extern uint8_t l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
 lean_object* l_Lean_Elab_Command_CommandElabM_MonadQuotation___closed__3;
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSection___closed__1;
+extern lean_object* l___private_Init_Lean_Elab_Term_8__elabTermUsing___main___closed__3;
 extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__4;
 extern lean_object* l_Lean_initAttr;
 lean_object* l_Lean_Elab_Command_logTrace___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -4367,7 +4367,7 @@ x_10 = lean_unsigned_to_nat(2u);
 x_11 = lean_alloc_ctor(7, 2, 0);
 lean_ctor_set(x_11, 0, x_10);
 lean_ctor_set(x_11, 1, x_9);
-x_12 = l___private_Init_Lean_Elab_Term_9__elabTermUsing___main___closed__3;
+x_12 = l___private_Init_Lean_Elab_Term_8__elabTermUsing___main___closed__3;
 x_13 = lean_alloc_ctor(9, 2, 0);
 lean_ctor_set(x_13, 0, x_12);
 lean_ctor_set(x_13, 1, x_11);
@ -8620,7 +8620,7 @@ x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
 if (x_5 == 0)
 {
 uint8_t x_6; 
-x_6 = l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
+x_6 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 if (x_6 == 0)
 {
 lean_object* x_7; lean_object* x_8; 
@ -8798,7 +8798,7 @@ if (x_11 == 0)
 {
 uint8_t x_14; 
 lean_dec(x_9);
-x_14 = l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
+x_14 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 if (x_14 == 0)
 {
 lean_object* x_15; lean_object* x_16; 
--- a/stage0/stdlib/Init/Lean/Elab/Declaration.c
+++ b/stage0/stdlib/Init/Lean/Elab/Declaration.c
@ -67,6 +67,7 @@ extern lean_object* l_Lean_Parser_Term_id___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Command_elabStructure___rarg(lean_object*);
 lean_object* l_Lean_Elab_Command_elabAxiom(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabInstance___closed__1;
+lean_object* l_Lean_Elab_Command_elabConstant___closed__11;
 extern lean_object* l_Lean_Parser_Command_def___elambda__1___closed__2;
 extern lean_object* l_Lean_Parser_Command_declValSimple___elambda__1___closed__2;
 extern lean_object* l_Lean_Meta_registerInstanceAttr___closed__1;
@ -95,7 +96,9 @@ extern lean_object* l_Lean_Elab_Command_withDeclId___closed__3;
 lean_object* l_Lean_Elab_Command_elabAxiom___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_sortDeclLevelParams(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabClassInductive___boxed(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_nullKind___closed__2;
 extern lean_object* l_Lean_mkReducibilityAttrs___closed__4;
+lean_object* l_Lean_Elab_Command_elabConstant___closed__10;
 lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Command_2__getState(lean_object*, lean_object*);
 lean_object* l_List_drop___main___rarg(lean_object*, lean_object*);
@ -459,6 +462,28 @@ lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
+lean_object* _init_l_Lean_Elab_Command_elabConstant___closed__10() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Array_empty___closed__1;
+x_2 = l_Lean_Elab_Command_elabConstant___closed__9;
+x_3 = lean_array_push(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Elab_Command_elabConstant___closed__11() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_nullKind___closed__2;
+x_2 = l_Lean_Elab_Command_elabConstant___closed__10;
+x_3 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_3, 0, x_1);
+lean_ctor_set(x_3, 1, x_2);
+return x_3;
+}
+}
 lean_object* l_Lean_Elab_Command_elabConstant(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
@ -504,7 +529,7 @@ x_27 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_27, 0, x_26);
 lean_ctor_set(x_27, 1, x_25);
 x_28 = lean_array_push(x_22, x_27);
-x_29 = l_Lean_Elab_Command_elabConstant___closed__9;
+x_29 = l_Lean_Elab_Command_elabConstant___closed__11;
 x_30 = lean_array_push(x_28, x_29);
 x_31 = l_Lean_Parser_Term_app___elambda__1___closed__2;
 x_32 = lean_alloc_ctor(1, 2, 0);
@ -4897,6 +4922,10 @@ l_Lean_Elab_Command_elabConstant___closed__8 = _init_l_Lean_Elab_Command_elabCon
 lean_mark_persistent(l_Lean_Elab_Command_elabConstant___closed__8);
 l_Lean_Elab_Command_elabConstant___closed__9 = _init_l_Lean_Elab_Command_elabConstant___closed__9();
 lean_mark_persistent(l_Lean_Elab_Command_elabConstant___closed__9);
+l_Lean_Elab_Command_elabConstant___closed__10 = _init_l_Lean_Elab_Command_elabConstant___closed__10();
+lean_mark_persistent(l_Lean_Elab_Command_elabConstant___closed__10);
+l_Lean_Elab_Command_elabConstant___closed__11 = _init_l_Lean_Elab_Command_elabConstant___closed__11();
+lean_mark_persistent(l_Lean_Elab_Command_elabConstant___closed__11);
 l_Lean_Elab_Command_elabInstance___closed__1 = _init_l_Lean_Elab_Command_elabInstance___closed__1();
 lean_mark_persistent(l_Lean_Elab_Command_elabInstance___closed__1);
 l_Lean_Elab_Command_elabExample___closed__1 = _init_l_Lean_Elab_Command_elabExample___closed__1();
--- a/stage0/stdlib/Init/Lean/Elab/Quotation.c
+++ b/stage0/stdlib/Init/Lean/Elab/Quotation.c
@ -17,6 +17,7 @@ lean_object* l_List_reverse___rarg(lean_object*);
 lean_object* l_Lean_Elab_Term_antiquotKind_x3f(lean_object*);
 lean_object* l_Lean_mkTermId(lean_object*);
 lean_object* l_List_head_x21___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__2___closed__2;
+extern lean_object* l___private_Init_Lean_Elab_Term_9__mkPairsAux___main___closed__4;
 lean_object* l_Lean_Prod_hasQuote___rarg___closed__1;
 lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__18;
 lean_object* l_Lean_Elab_Term_getEnv___rarg(lean_object*);
@ -90,6 +91,7 @@ extern lean_object* l_Lean_nameToExprAux___main___closed__4;
 lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__50;
 lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__15;
+extern uint8_t l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 extern lean_object* l_Prod_HasRepr___rarg___closed__1;
 lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_Quotation_7__getHeadInfo___spec__2___closed__1;
 lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__21;
@ -99,7 +101,6 @@ lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__5;
 lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__3;
 lean_object* l_Lean_Elab_Term_elabStxQuot___closed__1;
 extern lean_object* l_PersistentHashMap_mkCollisionNode___rarg___closed__1;
-extern lean_object* l___private_Init_Lean_Elab_Term_10__mkPairsAux___main___closed__6;
 lean_object* l_Lean_mkMVar(lean_object*);
 extern lean_object* l_Array_empty___closed__1;
 lean_object* l_List_mapM___main___at___private_Init_Lean_Elab_Quotation_10__getPatternVarsAux___main___spec__1(lean_object*, lean_object*, lean_object*);
@ -411,6 +412,7 @@ extern lean_object* l_Lean_Parser_Term_letPatDecl___elambda__1___closed__2;
 lean_object* l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_14__toPreterm___main___spec__4(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_getLCtx(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__17;
+extern lean_object* l___private_Init_Lean_Elab_Term_9__mkPairsAux___main___closed__6;
 lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_head_x21___at___private_Init_Lean_Elab_Quotation_7__getHeadInfo___spec__1(lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__57;
@ -511,7 +513,6 @@ lean_object* l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___close
 lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__11;
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___spec__1___closed__1;
 extern lean_object* l_Lean_Syntax_getKind___closed__3;
-extern lean_object* l___private_Init_Lean_Elab_Term_10__mkPairsAux___main___closed__4;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot(lean_object*);
 lean_object* l_Array_findMAux___main___at___private_Init_Lean_Elab_Quotation_4__elimAntiquotChoices___main___spec__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_mapM___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__8___closed__7;
@ -578,7 +579,6 @@ lean_object* l_Lean_mkConst(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__9;
 lean_object* l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__8;
 lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__37;
-extern uint8_t l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
 extern lean_object* l_Lean_Parser_Term_and___elambda__1___closed__1;
 lean_object* l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_14__toPreterm___main___spec__13(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_1__quoteName___main___closed__2;
@ -843,7 +843,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Elab_rootNamespace___closed__2;
-x_2 = l___private_Init_Lean_Elab_Term_10__mkPairsAux___main___closed__4;
+x_2 = l___private_Init_Lean_Elab_Term_9__mkPairsAux___main___closed__4;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@ -853,7 +853,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Prod_hasQuote___rarg___closed__1;
-x_2 = l___private_Init_Lean_Elab_Term_10__mkPairsAux___main___closed__6;
+x_2 = l___private_Init_Lean_Elab_Term_9__mkPairsAux___main___closed__6;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@ -5578,7 +5578,7 @@ x_68 = l_Lean_Syntax_isOfKind(x_66, x_67);
 if (x_68 == 0)
 {
 uint8_t x_69; 
-x_69 = l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
+x_69 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 if (x_69 == 0)
 {
 lean_dec(x_66);
@ -5655,7 +5655,7 @@ if (x_86 == 0)
 {
 uint8_t x_87; 
 lean_dec(x_85);
-x_87 = l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
+x_87 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 if (x_87 == 0)
 {
 lean_dec(x_84);
@ -10966,7 +10966,7 @@ x_45 = l_Lean_Syntax_isOfKind(x_43, x_44);
 if (x_45 == 0)
 {
 uint8_t x_46; 
-x_46 = l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
+x_46 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 if (x_46 == 0)
 {
 lean_dec(x_43);
@ -11043,7 +11043,7 @@ if (x_63 == 0)
 {
 uint8_t x_64; 
 lean_dec(x_62);
-x_64 = l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
+x_64 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 if (x_64 == 0)
 {
 lean_dec(x_61);
--- a/stage0/stdlib/Init/Lean/Elab/Syntax.c
+++ b/stage0/stdlib/Init/Lean/Elab/Syntax.c
--- a/stage0/stdlib/Init/Lean/Elab/SynthesizeSyntheticMVars.c
+++ b/stage0/stdlib/Init/Lean/Elab/SynthesizeSyntheticMVars.c
@ -63,13 +63,13 @@ lean_object* l_List_lengthAux___main___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___lambda__1___closed__1;
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_7__synthesizeUsingDefault___spec__1___lambda__1___closed__2;
-extern lean_object* l___private_Init_Lean_Elab_Term_8__postponeElabTerm___closed__1;
 lean_object* l_Lean_Elab_Term_logTrace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_9__getSomeSynthethicMVarsRef___boxed(lean_object*);
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_6__synthesizeSyntheticMVarsStep___spec__2___closed__4;
+extern lean_object* l___private_Init_Lean_Elab_Term_7__postponeElabTerm___closed__1;
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_6__synthesizeSyntheticMVarsStep___spec__2___closed__9;
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_6__synthesizeSyntheticMVarsStep___spec__2___closed__8;
 lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_9__getSomeSynthethicMVarsRef___rarg___lambda__1___boxed(lean_object*);
@ -996,7 +996,7 @@ if (lean_is_exclusive(x_4)) {
 lean_dec_ref(x_4);
 x_11 = lean_box(0);
 }
-x_18 = l___private_Init_Lean_Elab_Term_8__postponeElabTerm___closed__1;
+x_18 = l___private_Init_Lean_Elab_Term_7__postponeElabTerm___closed__1;
 lean_inc(x_3);
 x_19 = lean_name_mk_string(x_3, x_18);
 x_20 = lean_ctor_get(x_9, 0);
--- a/stage0/stdlib/Init/Lean/Elab/Tactic/Basic.c
+++ b/stage0/stdlib/Init/Lean/Elab/Tactic/Basic.c
@ -50,6 +50,7 @@ lean_object* l_Lean_Elab_Tactic_trace(lean_object*, lean_object*, lean_object*,
 lean_object* l___private_Init_Lean_Elab_Tactic_Basic_1__evalTacticUsing(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_getLCtx___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_monadQuotation___closed__2;
+extern uint8_t l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 lean_object* l_Lean_Elab_Tactic_evalIntro___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_liftMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_declareBuiltinTactic(lean_object*, lean_object*, lean_object*, lean_object*);
@ -228,7 +229,6 @@ lean_object* l_Lean_Elab_Tactic_withMVarContext___rarg___boxed(lean_object*, lea
 lean_object* l_Lean_Elab_Tactic_logTrace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_io_ref_reset(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_withFreshMacroScope___rarg(lean_object*, lean_object*, lean_object*);
-extern lean_object* l___private_Init_Lean_Elab_Term_9__elabTermUsing___main___closed__3;
 lean_object* l_Lean_SMap_empty___at_Lean_Elab_Tactic_mkBuiltinTacticTable___spec__1;
 lean_object* l_Lean_Elab_Tactic_throwError(lean_object*);
 lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_Tactic_evalTactic___main___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -292,7 +292,7 @@ lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_a
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_getCurrMacroScope___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_liftMetaTactic___closed__2;
-extern uint8_t l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
+extern lean_object* l___private_Init_Lean_Elab_Term_8__elabTermUsing___main___closed__3;
 extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__4;
 lean_object* l_Lean_Elab_Tactic_traceAtCmdPos(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_initAttr;
@ -3169,7 +3169,7 @@ x_10 = lean_unsigned_to_nat(2u);
 x_11 = lean_alloc_ctor(7, 2, 0);
 lean_ctor_set(x_11, 0, x_10);
 lean_ctor_set(x_11, 1, x_9);
-x_12 = l___private_Init_Lean_Elab_Term_9__elabTermUsing___main___closed__3;
+x_12 = l___private_Init_Lean_Elab_Term_8__elabTermUsing___main___closed__3;
 x_13 = lean_alloc_ctor(9, 2, 0);
 lean_ctor_set(x_13, 0, x_12);
 lean_ctor_set(x_13, 1, x_11);
@ -10188,7 +10188,7 @@ if (x_12 == 0)
 if (x_10 == 0)
 {
 uint8_t x_13; 
-x_13 = l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
+x_13 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 if (x_13 == 0)
 {
 lean_object* x_14; 
--- a/stage0/stdlib/Init/Lean/Elab/Term.c
+++ b/stage0/stdlib/Init/Lean/Elab/Term.c
--- a/stage0/stdlib/Init/Lean/Elab/TermApp.c
+++ b/stage0/stdlib/Init/Lean/Elab/TermApp.c
--- a/stage0/stdlib/Init/Lean/Elab/TermBinders.c
+++ b/stage0/stdlib/Init/Lean/Elab/TermBinders.c
@ -47,6 +47,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabFun___closed__2;
 lean_object* l_Lean_Elab_Term_elabForall___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__1;
 extern lean_object* l_Lean_Parser_Term_match___elambda__1___closed__1;
+extern uint8_t l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 extern lean_object* l_Prod_HasRepr___rarg___closed__1;
 lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_TermBinders_10__expandFunBindersAux___main___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_TermBinders_8__getFunBinderIdsAux_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -254,7 +255,6 @@ lean_object* l_Lean_Elab_Term_elabArrow___lambda__1___closed__3;
 extern lean_object* l_Lean_Parser_Term_simpleBinder___elambda__1___closed__2;
 extern lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__1;
 lean_object* l___private_Init_Lean_Elab_TermBinders_6__elabBinderViews___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern uint8_t l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
 lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_TermBinders_3__expandOptIdent(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabLet___closed__2;
@ -303,7 +303,7 @@ x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
 if (x_5 == 0)
 {
 uint8_t x_6; 
-x_6 = l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
+x_6 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 if (x_6 == 0)
 {
 lean_object* x_7; 
@ -539,7 +539,7 @@ lean_dec(x_3);
 x_19 = !lean_is_exclusive(x_18);
 if (x_19 == 0)
 {
-lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; 
+lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; 
 x_20 = lean_ctor_get(x_18, 0);
 x_21 = lean_box(0);
 x_22 = l_Lean_Expr_getOptParamDefault_x3f___closed__2;
@ -560,71 +560,73 @@ x_32 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_32, 0, x_31);
 lean_ctor_set(x_32, 1, x_30);
 x_33 = lean_array_push(x_27, x_32);
-x_34 = lean_array_push(x_33, x_1);
-x_35 = l_Lean_Parser_Term_app___elambda__1___closed__2;
-x_36 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_36, 0, x_35);
-lean_ctor_set(x_36, 1, x_34);
-x_37 = lean_array_push(x_27, x_36);
-x_38 = lean_array_push(x_37, x_17);
-x_39 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_39, 0, x_35);
-lean_ctor_set(x_39, 1, x_38);
-lean_ctor_set(x_18, 0, x_39);
+x_34 = lean_array_push(x_27, x_1);
+x_35 = lean_array_push(x_34, x_17);
+x_36 = l_Lean_nullKind___closed__2;
+x_37 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_37, 0, x_36);
+lean_ctor_set(x_37, 1, x_35);
+x_38 = lean_array_push(x_33, x_37);
+x_39 = l_Lean_Parser_Term_app___elambda__1___closed__2;
+x_40 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_40, 0, x_39);
+lean_ctor_set(x_40, 1, x_38);
+lean_ctor_set(x_18, 0, x_40);
 return x_18;
 }
 else
 {
-lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; 
-x_40 = lean_ctor_get(x_18, 0);
-x_41 = lean_ctor_get(x_18, 1);
+lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; 
+x_41 = lean_ctor_get(x_18, 0);
+x_42 = lean_ctor_get(x_18, 1);
+lean_inc(x_42);
 lean_inc(x_41);
-lean_inc(x_40);
 lean_dec(x_18);
-x_42 = lean_box(0);
-x_43 = l_Lean_Expr_getOptParamDefault_x3f___closed__2;
-x_44 = lean_name_mk_numeral(x_43, x_40);
-x_45 = l___private_Init_Lean_Elab_TermBinders_4__expandBinderModifier___closed__5;
-x_46 = l___private_Init_Lean_Elab_TermBinders_4__expandBinderModifier___closed__7;
-x_47 = lean_alloc_ctor(3, 4, 0);
-lean_ctor_set(x_47, 0, x_42);
-lean_ctor_set(x_47, 1, x_45);
-lean_ctor_set(x_47, 2, x_44);
-lean_ctor_set(x_47, 3, x_46);
-x_48 = l_Array_empty___closed__1;
-x_49 = lean_array_push(x_48, x_47);
-x_50 = l___private_Init_Lean_Elab_Term_5__expandCDot___closed__4;
-x_51 = lean_array_push(x_49, x_50);
-x_52 = l_Lean_Parser_Term_id___elambda__1___closed__2;
-x_53 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_53, 0, x_52);
-lean_ctor_set(x_53, 1, x_51);
-x_54 = lean_array_push(x_48, x_53);
-x_55 = lean_array_push(x_54, x_1);
-x_56 = l_Lean_Parser_Term_app___elambda__1___closed__2;
-x_57 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_57, 0, x_56);
-lean_ctor_set(x_57, 1, x_55);
-x_58 = lean_array_push(x_48, x_57);
-x_59 = lean_array_push(x_58, x_17);
-x_60 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_60, 0, x_56);
-lean_ctor_set(x_60, 1, x_59);
-x_61 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_61, 0, x_60);
-lean_ctor_set(x_61, 1, x_41);
-return x_61;
+x_43 = lean_box(0);
+x_44 = l_Lean_Expr_getOptParamDefault_x3f___closed__2;
+x_45 = lean_name_mk_numeral(x_44, x_41);
+x_46 = l___private_Init_Lean_Elab_TermBinders_4__expandBinderModifier___closed__5;
+x_47 = l___private_Init_Lean_Elab_TermBinders_4__expandBinderModifier___closed__7;
+x_48 = lean_alloc_ctor(3, 4, 0);
+lean_ctor_set(x_48, 0, x_43);
+lean_ctor_set(x_48, 1, x_46);
+lean_ctor_set(x_48, 2, x_45);
+lean_ctor_set(x_48, 3, x_47);
+x_49 = l_Array_empty___closed__1;
+x_50 = lean_array_push(x_49, x_48);
+x_51 = l___private_Init_Lean_Elab_Term_5__expandCDot___closed__4;
+x_52 = lean_array_push(x_50, x_51);
+x_53 = l_Lean_Parser_Term_id___elambda__1___closed__2;
+x_54 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_54, 0, x_53);
+lean_ctor_set(x_54, 1, x_52);
+x_55 = lean_array_push(x_49, x_54);
+x_56 = lean_array_push(x_49, x_1);
+x_57 = lean_array_push(x_56, x_17);
+x_58 = l_Lean_nullKind___closed__2;
+x_59 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_59, 0, x_58);
+lean_ctor_set(x_59, 1, x_57);
+x_60 = lean_array_push(x_55, x_59);
+x_61 = l_Lean_Parser_Term_app___elambda__1___closed__2;
+x_62 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_62, 0, x_61);
+lean_ctor_set(x_62, 1, x_60);
+x_63 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_63, 0, x_62);
+lean_ctor_set(x_63, 1, x_42);
+return x_63;
 }
 }
 }
 else
 {
-lean_object* x_62; 
+lean_object* x_64; 
 lean_dec(x_3);
-x_62 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_62, 0, x_1);
-lean_ctor_set(x_62, 1, x_4);
-return x_62;
+x_64 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_64, 0, x_1);
+lean_ctor_set(x_64, 1, x_4);
+return x_64;
 }
 }
 }
@ -3454,7 +3456,7 @@ x_6 = l_Lean_Syntax_isOfKind(x_1, x_5);
 if (x_6 == 0)
 {
 uint8_t x_7; 
-x_7 = l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
+x_7 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 if (x_7 == 0)
 {
 lean_object* x_8; 
@ -3953,30 +3955,30 @@ return x_5;
 lean_object* l___private_Init_Lean_Elab_TermBinders_8__getFunBinderIdsAux_x3f___main(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
-uint8_t x_6; lean_object* x_76; uint8_t x_77; 
-x_76 = l_Lean_Parser_Term_app___elambda__1___closed__2;
+uint8_t x_6; lean_object* x_120; uint8_t x_121; 
+x_120 = l_Lean_Parser_Term_app___elambda__1___closed__2;
 lean_inc(x_2);
-x_77 = l_Lean_Syntax_isOfKind(x_2, x_76);
-if (x_77 == 0)
+x_121 = l_Lean_Syntax_isOfKind(x_2, x_120);
+if (x_121 == 0)
 {
-uint8_t x_78; 
-x_78 = 0;
-x_6 = x_78;
-goto block_75;
+uint8_t x_122; 
+x_122 = 0;
+x_6 = x_122;
+goto block_119;
 }
 else
 {
-lean_object* x_79; lean_object* x_80; lean_object* x_81; uint8_t x_82; 
-x_79 = l_Lean_Syntax_getArgs(x_2);
-x_80 = lean_array_get_size(x_79);
-lean_dec(x_79);
-x_81 = lean_unsigned_to_nat(2u);
-x_82 = lean_nat_dec_eq(x_80, x_81);
-lean_dec(x_80);
-x_6 = x_82;
-goto block_75;
+lean_object* x_123; lean_object* x_124; lean_object* x_125; uint8_t x_126; 
+x_123 = l_Lean_Syntax_getArgs(x_2);
+x_124 = lean_array_get_size(x_123);
+lean_dec(x_123);
+x_125 = lean_unsigned_to_nat(2u);
+x_126 = lean_nat_dec_eq(x_124, x_125);
+lean_dec(x_124);
+x_6 = x_126;
+goto block_119;
 }
-block_75:
+block_119:
 {
 uint8_t x_7; 
 x_7 = l_coeDecidableEq(x_6);
@ -3989,7 +3991,7 @@ x_9 = l_Lean_Syntax_isOfKind(x_2, x_8);
 if (x_9 == 0)
 {
 uint8_t x_10; 
-x_10 = l___private_Init_Lean_Elab_Term_4__hasCDot___main___closed__1;
+x_10 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
 if (x_10 == 0)
 {
 lean_object* x_11; 
@ -4163,69 +4165,256 @@ return x_57;
 }
 else
 {
-if (x_1 == 0)
-{
-lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; uint8_t x_62; lean_object* x_63; lean_object* x_64; 
+lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; uint8_t x_63; 
 x_58 = lean_unsigned_to_nat(0u);
 x_59 = l_Lean_Syntax_getArg(x_2, x_58);
 x_60 = lean_unsigned_to_nat(1u);
 x_61 = l_Lean_Syntax_getArg(x_2, x_60);
-lean_dec(x_2);
-x_62 = 0;
-x_63 = l___private_Init_Lean_Elab_TermBinders_8__getFunBinderIdsAux_x3f___main(x_62, x_59, x_3, x_4, x_5);
-x_64 = lean_ctor_get(x_63, 0);
-lean_inc(x_64);
-if (lean_obj_tag(x_64) == 0)
+x_62 = l_Lean_nullKind___closed__2;
+lean_inc(x_61);
+x_63 = l_Lean_Syntax_isOfKind(x_61, x_62);
+if (x_63 == 0)
 {
-uint8_t x_65; 
+uint8_t x_64; 
+x_64 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
+if (x_64 == 0)
+{
+lean_object* x_65; 
 lean_dec(x_61);
-x_65 = !lean_is_exclusive(x_63);
-if (x_65 == 0)
+lean_dec(x_59);
+x_65 = l_Lean_Syntax_isSimpleTermId_x3f(x_2);
+lean_dec(x_2);
+if (lean_obj_tag(x_65) == 0)
 {
-lean_object* x_66; 
-x_66 = lean_ctor_get(x_63, 0);
-lean_dec(x_66);
-return x_63;
+lean_object* x_66; lean_object* x_67; 
+lean_dec(x_3);
+x_66 = lean_box(0);
+x_67 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_67, 0, x_66);
+lean_ctor_set(x_67, 1, x_5);
+return x_67;
 }
 else
 {
-lean_object* x_67; lean_object* x_68; 
-x_67 = lean_ctor_get(x_63, 1);
-lean_inc(x_67);
-lean_dec(x_63);
-x_68 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_68, 0, x_64);
-lean_ctor_set(x_68, 1, x_67);
-return x_68;
+uint8_t x_68; 
+x_68 = !lean_is_exclusive(x_65);
+if (x_68 == 0)
+{
+lean_object* x_69; lean_object* x_70; lean_object* x_71; 
+x_69 = lean_ctor_get(x_65, 0);
+x_70 = lean_array_push(x_3, x_69);
+lean_ctor_set(x_65, 0, x_70);
+x_71 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_71, 0, x_65);
+lean_ctor_set(x_71, 1, x_5);
+return x_71;
+}
+else
+{
+lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; 
+x_72 = lean_ctor_get(x_65, 0);
+lean_inc(x_72);
+lean_dec(x_65);
+x_73 = lean_array_push(x_3, x_72);
+x_74 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_74, 0, x_73);
+x_75 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_75, 0, x_74);
+lean_ctor_set(x_75, 1, x_5);
+return x_75;
+}
 }
 }
 else
 {
-lean_object* x_69; lean_object* x_70; uint8_t x_71; 
-x_69 = lean_ctor_get(x_63, 1);
-lean_inc(x_69);
-lean_dec(x_63);
-x_70 = lean_ctor_get(x_64, 0);
-lean_inc(x_70);
-lean_dec(x_64);
-x_71 = 1;
-x_1 = x_71;
-x_2 = x_61;
-x_3 = x_70;
-x_5 = x_69;
+lean_dec(x_2);
+if (x_1 == 0)
+{
+lean_object* x_76; uint8_t x_77; lean_object* x_78; lean_object* x_79; 
+x_76 = l_Lean_Syntax_getArg(x_61, x_58);
+lean_dec(x_61);
+x_77 = 0;
+x_78 = l___private_Init_Lean_Elab_TermBinders_8__getFunBinderIdsAux_x3f___main(x_77, x_59, x_3, x_4, x_5);
+x_79 = lean_ctor_get(x_78, 0);
+lean_inc(x_79);
+if (lean_obj_tag(x_79) == 0)
+{
+uint8_t x_80; 
+lean_dec(x_76);
+x_80 = !lean_is_exclusive(x_78);
+if (x_80 == 0)
+{
+lean_object* x_81; 
+x_81 = lean_ctor_get(x_78, 0);
+lean_dec(x_81);
+return x_78;
+}
+else
+{
+lean_object* x_82; lean_object* x_83; 
+x_82 = lean_ctor_get(x_78, 1);
+lean_inc(x_82);
+lean_dec(x_78);
+x_83 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_83, 0, x_79);
+lean_ctor_set(x_83, 1, x_82);
+return x_83;
+}
+}
+else
+{
+lean_object* x_84; lean_object* x_85; uint8_t x_86; 
+x_84 = lean_ctor_get(x_78, 1);
+lean_inc(x_84);
+lean_dec(x_78);
+x_85 = lean_ctor_get(x_79, 0);
+lean_inc(x_85);
+lean_dec(x_79);
+x_86 = 1;
+x_1 = x_86;
+x_2 = x_76;
+x_3 = x_85;
+x_5 = x_84;
 goto _start;
 }
 }
 else
 {
-lean_object* x_73; lean_object* x_74; 
+lean_object* x_88; lean_object* x_89; 
+lean_dec(x_61);
+lean_dec(x_59);
 lean_dec(x_3);
+x_88 = lean_box(0);
+x_89 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_89, 0, x_88);
+lean_ctor_set(x_89, 1, x_5);
+return x_89;
+}
+}
+}
+else
+{
+lean_object* x_90; lean_object* x_91; uint8_t x_92; uint8_t x_93; 
+x_90 = l_Lean_Syntax_getArgs(x_61);
+x_91 = lean_array_get_size(x_90);
+lean_dec(x_90);
+x_92 = lean_nat_dec_eq(x_91, x_60);
+lean_dec(x_91);
+x_93 = l_coeDecidableEq(x_92);
+if (x_93 == 0)
+{
+lean_object* x_94; 
+lean_dec(x_61);
+lean_dec(x_59);
+x_94 = l_Lean_Syntax_isSimpleTermId_x3f(x_2);
 lean_dec(x_2);
-x_73 = lean_box(0);
-x_74 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_74, 0, x_73);
-lean_ctor_set(x_74, 1, x_5);
-return x_74;
+if (lean_obj_tag(x_94) == 0)
+{
+lean_object* x_95; lean_object* x_96; 
+lean_dec(x_3);
+x_95 = lean_box(0);
+x_96 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_96, 0, x_95);
+lean_ctor_set(x_96, 1, x_5);
+return x_96;
+}
+else
+{
+uint8_t x_97; 
+x_97 = !lean_is_exclusive(x_94);
+if (x_97 == 0)
+{
+lean_object* x_98; lean_object* x_99; lean_object* x_100; 
+x_98 = lean_ctor_get(x_94, 0);
+x_99 = lean_array_push(x_3, x_98);
+lean_ctor_set(x_94, 0, x_99);
+x_100 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_100, 0, x_94);
+lean_ctor_set(x_100, 1, x_5);
+return x_100;
+}
+else
+{
+lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; 
+x_101 = lean_ctor_get(x_94, 0);
+lean_inc(x_101);
+lean_dec(x_94);
+x_102 = lean_array_push(x_3, x_101);
+x_103 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_103, 0, x_102);
+x_104 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_104, 0, x_103);
+lean_ctor_set(x_104, 1, x_5);
+return x_104;
+}
+}
+}
+else
+{
+lean_dec(x_2);
+if (x_1 == 0)
+{
+lean_object* x_105; uint8_t x_106; lean_object* x_107; lean_object* x_108; 
+x_105 = l_Lean_Syntax_getArg(x_61, x_58);
+lean_dec(x_61);
+x_106 = 0;
+x_107 = l___private_Init_Lean_Elab_TermBinders_8__getFunBinderIdsAux_x3f___main(x_106, x_59, x_3, x_4, x_5);
+x_108 = lean_ctor_get(x_107, 0);
+lean_inc(x_108);
+if (lean_obj_tag(x_108) == 0)
+{
+uint8_t x_109; 
+lean_dec(x_105);
+x_109 = !lean_is_exclusive(x_107);
+if (x_109 == 0)
+{
+lean_object* x_110; 
+x_110 = lean_ctor_get(x_107, 0);
+lean_dec(x_110);
+return x_107;
+}
+else
+{
+lean_object* x_111; lean_object* x_112; 
+x_111 = lean_ctor_get(x_107, 1);
+lean_inc(x_111);
+lean_dec(x_107);
+x_112 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_112, 0, x_108);
+lean_ctor_set(x_112, 1, x_111);
+return x_112;
+}
+}
+else
+{
+lean_object* x_113; lean_object* x_114; uint8_t x_115; 
+x_113 = lean_ctor_get(x_107, 1);
+lean_inc(x_113);
+lean_dec(x_107);
+x_114 = lean_ctor_get(x_108, 0);
+lean_inc(x_114);
+lean_dec(x_108);
+x_115 = 1;
+x_1 = x_115;
+x_2 = x_105;
+x_3 = x_114;
+x_5 = x_113;
+goto _start;
+}
+}
+else
+{
+lean_object* x_117; lean_object* x_118; 
+lean_dec(x_61);
+lean_dec(x_59);
+lean_dec(x_3);
+x_117 = lean_box(0);
+x_118 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_118, 0, x_117);
+lean_ctor_set(x_118, 1, x_5);
+return x_118;
+}
+}
 }
 }
 }