chore: update stage0

2019-12-11 16:27:18 -08:00 · 2019-12-11 16:27:18 -08:00 · 8f21f6a062
commit 8f21f6a062
parent e7d818fe61
19 changed files with 6042 additions and 1242 deletions
--- a/stage0/src/Init/Core.lean
+++ b/stage0/src/Init/Core.lean
@ -340,7 +340,7 @@ class HasNeg      (α : Type u) := (neg : α → α)
 class HasSub      (α : Type u) := (sub : α → α → α)
 class HasDiv      (α : Type u) := (div : α → α → α)
 class HasMod      (α : Type u) := (mod : α → α → α)
-class HasModn     (α : Type u) := (modn : α → Nat → α)
+class HasModN     (α : Type u) := (modn : α → Nat → α)
 class HasLessEq   (α : Type u) := (LessEq : α → α → Prop)
 class HasLess     (α : Type u) := (Less : α → α → Prop)
 class HasBeq      (α : Type u) := (beq : α → α → Bool)
@ -353,15 +353,12 @@ class HasEmptyc   (α : Type u) := (emptyc : α)
 class HasPow (α : Type u) (β : Type v) :=
 (pow : α → β → α)

-export HasAndthen (andthen)
-export HasPow (pow)
-
 infix `+`        := HasAdd.add
 infix `*`        := HasMul.mul
 infix `-`        := HasSub.sub
 infix `/`        := HasDiv.div
 infix `%`        := HasMod.mod
-infix `%ₙ`       := HasModn.modn
+infix `%ₙ`       := HasModN.modn
 prefix `-`       := HasNeg.neg
 infix `<=`       := HasLessEq.LessEq
 infix `≤`        := HasLessEq.LessEq
@ -382,8 +379,6 @@ infix `↔`        := Iff
 infixr `<|>`     := HasOrelse.orelse
 infixr `>>`      := HasAndthen.andthen

-export HasAppend (append)
-
@[reducible] def GreaterEq {α : Type u} [HasLessEq α] (a b : α) : Prop := HasLessEq.LessEq b a
@[reducible] def Greater {α : Type u} [HasLess α] (a b : α) : Prop     := HasLess.Less b a

--- a/stage0/src/Init/Data/DList.lean
+++ b/stage0/src/Init/Data/DList.lean
@ -21,7 +21,7 @@ variables {α : Type u}
 open List

 def ofList (l : List α) : DList α :=
-⟨append l, fun t => (appendNil l).symm ▸ rfl⟩
+⟨HasAppend.append l, fun t => (appendNil l).symm ▸ rfl⟩

 def empty : DList α :=
 ⟨id, fun t => rfl⟩
--- a/stage0/src/Init/Data/Fin/Basic.lean
+++ b/stage0/src/Init/Data/Fin/Basic.lean
@ -81,7 +81,7 @@ instance : HasSub (Fin n)         := ⟨Fin.sub⟩
 instance : HasMul (Fin n)         := ⟨Fin.mul⟩
 instance : HasMod (Fin n)         := ⟨Fin.mod⟩
 instance : HasDiv (Fin n)         := ⟨Fin.div⟩
-instance : HasModn (Fin n)        := ⟨Fin.modn⟩
+instance : HasModN (Fin n)        := ⟨Fin.modn⟩

 theorem eqOfVeq : ∀ {i j : Fin n}, (val i) = (val j) → i = j
 | ⟨iv, ilt₁⟩, ⟨.(iv), ilt₂⟩, rfl => rfl
--- a/stage0/src/Init/Data/UInt.lean
+++ b/stage0/src/Init/Data/UInt.lean
@ -43,7 +43,7 @@ instance : HasAdd UInt8      := ⟨UInt8.add⟩
 instance : HasSub UInt8      := ⟨UInt8.sub⟩
 instance : HasMul UInt8      := ⟨UInt8.mul⟩
 instance : HasMod UInt8      := ⟨UInt8.mod⟩
-instance : HasModn UInt8     := ⟨UInt8.modn⟩
+instance : HasModN UInt8     := ⟨UInt8.modn⟩
 instance : HasDiv UInt8      := ⟨UInt8.div⟩
 instance : HasLess UInt8     := ⟨UInt8.lt⟩
 instance : HasLessEq UInt8   := ⟨UInt8.le⟩
@ -102,7 +102,7 @@ instance : HasAdd UInt16      := ⟨UInt16.add⟩
 instance : HasSub UInt16      := ⟨UInt16.sub⟩
 instance : HasMul UInt16      := ⟨UInt16.mul⟩
 instance : HasMod UInt16      := ⟨UInt16.mod⟩
-instance : HasModn UInt16     := ⟨UInt16.modn⟩
+instance : HasModN UInt16     := ⟨UInt16.modn⟩
 instance : HasDiv UInt16      := ⟨UInt16.div⟩
 instance : HasLess UInt16     := ⟨UInt16.lt⟩
 instance : HasLessEq UInt16   := ⟨UInt16.le⟩
@ -161,7 +161,7 @@ instance : HasAdd UInt32      := ⟨UInt32.add⟩
 instance : HasSub UInt32      := ⟨UInt32.sub⟩
 instance : HasMul UInt32      := ⟨UInt32.mul⟩
 instance : HasMod UInt32      := ⟨UInt32.mod⟩
-instance : HasModn UInt32     := ⟨UInt32.modn⟩
+instance : HasModN UInt32     := ⟨UInt32.modn⟩
 instance : HasDiv UInt32      := ⟨UInt32.div⟩
 instance : HasLess UInt32     := ⟨UInt32.lt⟩
 instance : HasLessEq UInt32   := ⟨UInt32.le⟩
@ -234,7 +234,7 @@ instance : HasAdd UInt64      := ⟨UInt64.add⟩
 instance : HasSub UInt64      := ⟨UInt64.sub⟩
 instance : HasMul UInt64      := ⟨UInt64.mul⟩
 instance : HasMod UInt64      := ⟨UInt64.mod⟩
-instance : HasModn UInt64     := ⟨UInt64.modn⟩
+instance : HasModN UInt64     := ⟨UInt64.modn⟩
 instance : HasDiv UInt64      := ⟨UInt64.div⟩
 instance : HasLess UInt64     := ⟨UInt64.lt⟩
 instance : HasLessEq UInt64   := ⟨UInt64.le⟩
@ -311,7 +311,7 @@ instance : HasAdd USize      := ⟨USize.add⟩
 instance : HasSub USize      := ⟨USize.sub⟩
 instance : HasMul USize      := ⟨USize.mul⟩
 instance : HasMod USize      := ⟨USize.mod⟩
-instance : HasModn USize     := ⟨USize.modn⟩
+instance : HasModN USize     := ⟨USize.modn⟩
 instance : HasDiv USize      := ⟨USize.div⟩
 instance : HasLess USize     := ⟨USize.lt⟩
 instance : HasLessEq USize   := ⟨USize.le⟩
--- a/stage0/src/Init/Lean/Elab.lean
+++ b/stage0/src/Init/Lean/Elab.lean
@ -10,3 +10,4 @@ import Init.Lean.Elab.ElabStrategyAttrs
 import Init.Lean.Elab.Command
 import Init.Lean.Elab.Term
 import Init.Lean.Elab.Frontend
+import Init.Lean.Elab.BuiltinNotation
--- a/stage0/src/Init/Lean/Elab/BuiltinNotation.lean
+++ b/stage0/src/Init/Lean/Elab/BuiltinNotation.lean
@ -0,0 +1,81 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Elab.Term
+
+namespace Lean
+namespace Elab
+namespace Term
+
+@[builtinTermElab dollar] def elabDollar : TermElab :=
+fun stx expectedType? => do
+  -- term `$` term
+  let f := stx.getArg 0;
+  let a := stx.getArg 2;
+  elabTerm (mkAppStx f #[a]) expectedType?
+
+def elabInfix (f : Syntax) : TermElab :=
+fun stx expectedType? => do
+  -- term `op` term
+  let a := stx.getArg 0;
+  let b := stx.getArg 2;
+  elabTerm (mkAppStx f #[a, b]) expectedType?
+
+def elabInfixOp (op : Name) : TermElab :=
+fun stx expectedType? => elabInfix (mkTermId (stx.getArg 1) op) stx expectedType?
+
+@[builtinTermElab add] def elabAdd : TermElab := elabInfixOp `HasAdd.add
+@[builtinTermElab sub] def elabSub : TermElab := elabInfixOp `HasSub.sub
+@[builtinTermElab mul] def elabMul : TermElab := elabInfixOp `HasMul.mul
+@[builtinTermElab div] def elabDiv : TermElab := elabInfixOp `HasDiv.div
+@[builtinTermElab mod] def elabMod : TermElab := elabInfixOp `HasMod.mod
+@[builtinTermElab modN] def elabModN : TermElab := elabInfixOp `HasModN.modn
+@[builtinTermElab pow] def elabPow : TermElab := elabInfixOp `HasPow.pow
+
+@[builtinTermElab le] def elabLE : TermElab := elabInfixOp `HasLessEq.LessEq
+@[builtinTermElab ge] def elabGE : TermElab := elabInfixOp `GreaterEq
+@[builtinTermElab lt] def elabLT : TermElab := elabInfixOp `HasLess.Less
+@[builtinTermElab gt] def elabGT : TermElab := elabInfixOp `Greater
+@[builtinTermElab eq] def elabEq : TermElab := elabInfixOp `Eq
+@[builtinTermElab ne] def elabNe : TermElab := elabInfixOp `Ne
+@[builtinTermElab beq] def elabBEq : TermElab := elabInfixOp `HasBeq.beq
+@[builtinTermElab bne] def elabBNe : TermElab := elabInfixOp `bne
+@[builtinTermElab heq] def elabHEq : TermElab := elabInfixOp `HEq
+@[builtinTermElab equiv] def elabEquiv : TermElab := elabInfixOp `HasEquiv.Equiv
+
+@[builtinTermElab and] def elabAnd : TermElab := elabInfixOp `And
+@[builtinTermElab or] def elabOr : TermElab := elabInfixOp `Or
+@[builtinTermElab iff] def elabIff : TermElab := elabInfixOp `Iff
+
+@[builtinTermElab band] def elabBAnd : TermElab := elabInfixOp `and
+@[builtinTermElab bor] def elabBOr : TermElab := elabInfixOp `or
+
+@[builtinTermElab append] def elabAppend : TermElab := elabInfixOp `HasAppend.append
+@[builtinTermElab cons] def elabCons : TermElab := elabInfixOp `List.cons
+
+@[builtinTermElab andthen] def elabAndThen : TermElab := elabInfixOp `HasAndthen.andthen
+-- @[builtinTermElab bind] def elabBind : TermElab := elabInfixOp `HasBind.bind
+
+@[builtinTermElab seq] def elabseq : TermElab := elabInfixOp `HasSeq.seq
+@[builtinTermElab seqLeft] def elabseqLeft : TermElab := elabInfixOp `HasSeqLeft.seqLeft
+@[builtinTermElab seqRight] def elabseqRight : TermElab := elabInfixOp `HasSeqRight.seqRight
+
+@[builtinTermElab map] def elabMap : TermElab := elabInfixOp `Functor.map
+@[builtinTermElab mapRev] def elabMapRev : TermElab := elabInfixOp `Functor.mapRev
+@[builtinTermElab mapConst] def elabMapConst : TermElab := elabInfixOp `Functor.mapConst
+@[builtinTermElab mapConstRev] def elabMapConstRev : TermElab := elabInfixOp `Functor.mapConstRev
+
+@[builtinTermElab orelse] def elabOrElse : TermElab := elabInfixOp `HasOrelse.orelse
+@[builtinTermElab orM] def elabOrM : TermElab := elabInfixOp `orM
+@[builtinTermElab andM] def elabAndM : TermElab := elabInfixOp `andM
+
+/-
+@[builtinTermElab] def elabsubst : TermElab := elabInfixOp infixR " ▸ " 75
+-/
+
+end Term
+end Elab
+end Lean
--- a/stage0/src/Init/Lean/Elab/Term.lean
+++ b/stage0/src/Init/Lean/Elab/Term.lean
@ -24,13 +24,16 @@ structure Context extends Meta.Context :=
 (macroStack  : List Syntax := [])
 (mayPostpone : Bool := true)

-inductive SyntheticMVarInfo
-| typeClass : SyntheticMVarInfo
-| tactic (tacticCode : Syntax) : SyntheticMVarInfo
-| postponed (macroStack : List Syntax) : SyntheticMVarInfo
+inductive SyntheticMVarKind
+| typeClass
+| tactic (tacticCode : Syntax)
+| postponed (macroStack : List Syntax)
+
+structure SyntheticMVarDecl :=
+(mvarId : MVarId) (ref : Syntax) (kind : SyntheticMVarKind)

 structure State extends Meta.State :=
-(syntheticMVars  : List (MVarId × SyntheticMVarInfo) := [])
+(syntheticMVars  : List SyntheticMVarDecl := [])
 (messages        : MessageLog := {})
 (instImplicitIdx : Nat := 1)
 (anonymousIdx    : Nat := 1)
@ -108,6 +111,7 @@ fun ctx s => match x ctx.toContext s.toState with
  | EStateM.Result.error ex newS => EStateM.Result.error (Exception.meta ex) { toState := newS, .. s }

 def getEnv : TermElabM Environment := do s ← get; pure s.env
+def getMCtx : TermElabM MetavarContext := do s ← get; pure s.mctx
 def getNamespace : TermElabM Name := do ctx ← read; pure ctx.ns
 def getOpenDecls : TermElabM (List OpenDecl) := do ctx ← read; pure ctx.openDecls
 def getLCtx : TermElabM LocalContext := do ctx ← read; pure ctx.lctx
@ -115,6 +119,10 @@ def getLocalInsts : TermElabM LocalInstances := do ctx ← read; pure ctx.localI
 def getOptions : TermElabM Options       := do ctx ← read; pure ctx.config.opts
 def getTraceState : TermElabM TraceState := do s ← get; pure s.traceState
 def setTraceState (traceState : TraceState) : TermElabM Unit := modify $ fun s => { traceState := traceState, .. s }
+def isExprMVarAssigned (mvarId : MVarId) : TermElabM Bool := do mctx ← getMCtx; pure $ mctx.isExprAssigned mvarId
+def getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl := do mctx ← getMCtx; pure $ mctx.getDecl mvarId
+def assignExprMVar (mvarId : MVarId) (val : Expr) : TermElabM Unit := modify $ fun s => { mctx := s.mctx.assignExpr mvarId val, .. s }
+
 def addContext (msg : MessageData) : TermElabM MessageData := do
 ctx ← read;
 s   ← get;
@ -136,12 +144,17 @@ def whnfForall (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnfForall e
 def instantiateMVars (e : Expr) : TermElabM Expr := liftMetaM $ Meta.instantiateMVars e
 def isClass (t : Expr) : TermElabM (Option Name) := liftMetaM $ Meta.isClass t
 def mkFreshLevelMVar : TermElabM Level := liftMetaM $ Meta.mkFreshLevelMVar
-def mkForall (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM $ Meta.mkForall xs e
 def mkFreshExprMVar (type? : Option Expr := none) (synthetic : Bool := false) (userName? : Name := Name.anonymous) : TermElabM Expr :=
 match type? with
 | some type => liftMetaM $ Meta.mkFreshExprMVar type userName? synthetic
 | none      => liftMetaM $ do u ← Meta.mkFreshLevelMVar; Meta.mkFreshExprMVar (mkSort u) userName? synthetic

+def mkForall (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM $ Meta.mkForall xs e
+def trySynthInstance (type : Expr) : TermElabM (LOption Expr) := liftMetaM $ Meta.trySynthInstance type
+
+def registerSyntheticMVar (mvarId : MVarId) (ref : Syntax) (kind : SyntheticMVarKind) : TermElabM Unit :=
+modify $ fun s => { syntheticMVars := { mvarId := mvarId, ref := ref, kind := kind } :: s.syntheticMVars, .. s }
+
@[inline] def withoutPostponing {α} (x : TermElabM α) : TermElabM α :=
 adaptReader (fun (ctx : Context) => { mayPostpone := false, .. ctx }) x

@ -204,7 +217,7 @@ let instIdx := s.instImplicitIdx;
 modify $ fun s => { instImplicitIdx := s.instImplicitIdx + 1, .. s};
 pure $ (`_inst).appendIndexAfter instIdx

-def mkHole := mkNode `Lean.Parser.Term.hole [mkAtom "_"]
+def mkHole := mkNode `Lean.Parser.Term.hole #[mkAtom "_"]

 /--
  Given syntax of the forms
@ -333,7 +346,7 @@ fun stx _ =>
    mkForall xs e

 def mkExplicitBinder (n : Syntax) (type : Syntax) : Syntax :=
-mkNode `Lean.Parser.Term.explicitBinder [mkAtom "(", mkNullNode [n], mkNullNode [mkAtom ":", type], mkNullNode [], mkAtom ")"]
+mkNode `Lean.Parser.Term.explicitBinder #[mkAtom "(", mkNullNode #[n], mkNullNode #[mkAtom ":", type], mkNullNode, mkAtom ")"]

@[builtinTermElab arrow] def elabArrow : TermElab :=
 fun stx expectedType? => do
@ -341,7 +354,7 @@ fun stx expectedType? => do
  let id     := mkIdentFrom stx.val a;
  let dom    := stx.getArg 0;
  let rng    := stx.getArg 2;
-  let newStx := mkNode `Lean.Parser.Term.forall [mkAtom "forall", mkNullNode [mkExplicitBinder id dom], mkAtom ",", rng];
+  let newStx := mkNode `Lean.Parser.Term.forall #[mkAtom "forall", mkNullNode #[mkExplicitBinder id dom], mkAtom ",", rng];
  elabTerm newStx expectedType?

@[builtinTermElab depArrow] def elabDepArrow : TermElab :=
@ -364,14 +377,18 @@ fun stx expectedType? =>
    -- TODO: handle parenSpecial
    elabTerm term expectedType?

+def mkTermId (ref : Syntax) (n : Name) : Syntax :=
+let id := mkIdentFrom ref n;
+mkNode `Lean.Parser.Term.id #[id, mkNullNode]
+
@[builtinTermElab «listLit»] def elabListLit : TermElab :=
 fun stx expectedType? => do
  let openBkt  := stx.getArg 0;
  let args     := stx.getArg 1;
  let closeBkt := stx.getArg 2;
-  let consId   := mkIdentFrom openBkt `List.cons;
-  let nilId    := mkIdentFrom closeBkt `List.nil;
-  let newStx   := args.foldSepArgs (fun arg r => mkAppStx consId #[arg, r]) nilId;
+  let consId   := mkTermId openBkt `List.cons;
+  let nilId    := mkTermId closeBkt `List.nil;
+  let newStx   := args.foldSepRevArgs (fun arg r => mkAppStx consId #[arg, r]) nilId;
  elabTerm newStx expectedType?

 def elabExplicitUniv (stx : Syntax) : TermElabM (List Level) :=
@ -453,6 +470,9 @@ match expectedType? with
  condM (isDefEq eType expectedType)
    (pure e)
    (do -- TODO try `HasCoe`
+        e ← instantiateMVars e;
+        eType ← instantiateMVars eType;
+        expectedType ← instantiateMVars expectedType;
        let msg : MessageData :=
          "type mismatch" ++ indentExpr e
          ++ Format.line ++ "has type" ++ indentExpr eType
@ -460,57 +480,80 @@ match expectedType? with
        logErrorAndThrow ref msg)

 /-- Consume parameters of the form `(x : A := val)` and `(x : A . tactic)` -/
-def consumeDefaultParams (ref : Syntax) (expectedType? : Option Expr) : Expr → Expr → TermElabM Expr
+def consumeDefaultParams (ref : Syntax) : Expr → Expr → TermElabM Expr
 | eType, e =>
  -- TODO
-  ensureHasType ref expectedType? eType e
+  pure e
+
+def synthesizeInstMVar (ref : Syntax) (instMVar : MVarId) : TermElabM Unit :=
+condM (isExprMVarAssigned instMVar) (pure ()) $ do
+  instMVarDecl ← getMVarDecl instMVar;
+  let type := instMVarDecl.type;
+  type ← instantiateMVars type;
+  result ← trySynthInstance type;
+  match result with
+  | LOption.some val => assignExprMVar instMVar val
+  | LOption.undef    => pure () -- we will try later
+  | LOption.none     => logErrorAndThrow ref ("failed to synthesize instance" ++ indentExpr type)
+
+def synthesizeInstMVars (ref : Syntax) (instMVars : Array MVarId) : TermElabM Unit :=
+instMVars.forM $ synthesizeInstMVar ref

 private partial def elabAppArgsAux (ref : Syntax) (args : Array Syntax) (expectedType? : Option Expr) (explicit : Bool)
-    : Nat → Array NamedArg → Expr → Expr → TermElabM Expr
-| argIdx, namedArgs, eType, e =>
-  if namedArgs.isEmpty && argIdx == args.size then
+    : Nat → Array NamedArg → Array MVarId → Expr → Expr → TermElabM Expr
+| argIdx, namedArgs, instMVars, eType, e => do
+  let finalize : Unit → TermElabM Expr := fun _ => do {
    -- all user explicit arguments have been consumed
-    if explicit then
-       ensureHasType ref expectedType? eType e
-    else
-       consumeDefaultParams ref expectedType? eType e
-  else do
-    eType ← whnfForall eType;
-    match eType with
-    | Expr.forallE n d b c =>
-      match namedArgs.findIdx? (fun namedArg => namedArg.name == n) with
-      | some idx => do
-        let arg       := namedArgs.get! idx;
-        let namedArgs := namedArgs.eraseIdx idx;
-        a ← elabTerm arg.val d;
-        elabAppArgsAux argIdx namedArgs (b.instantiate1 a) (mkApp e a)
-      | none =>
-        let processExplictArg : Unit → TermElabM Expr := fun _ => do {
-          if h : argIdx < args.size then do
-            a ← elabTerm (args.get ⟨argIdx, h⟩) d;
-            elabAppArgsAux (argIdx + 1) namedArgs (b.instantiate1 a) (mkApp e a)
-          else
-            logErrorAndThrow ref ("explicit parameter '" ++ n ++ "' is missing, unused named arguments " ++ toString (namedArgs.map $ fun narg => narg.name))
-        };
-        if explicit then
+    e ← if explicit then pure e else consumeDefaultParams ref eType e;
+    e ← ensureHasType ref expectedType? eType e;
+    synthesizeInstMVars ref instMVars;
+    pure e
+  };
+  eType ← whnfForall eType;
+  match eType with
+  | Expr.forallE n d b c =>
+    match namedArgs.findIdx? (fun namedArg => namedArg.name == n) with
+    | some idx => do
+      let arg       := namedArgs.get! idx;
+      let namedArgs := namedArgs.eraseIdx idx;
+      a ← elabTerm arg.val d;
+      elabAppArgsAux argIdx namedArgs instMVars (b.instantiate1 a) (mkApp e a)
+    | none =>
+      let processExplictArg : Unit → TermElabM Expr := fun _ => do {
+        if h : argIdx < args.size then do
+          a ← elabTerm (args.get ⟨argIdx, h⟩) d;
+          elabAppArgsAux (argIdx + 1) namedArgs instMVars (b.instantiate1 a) (mkApp e a)
+        else if namedArgs.isEmpty then
+          finalize ()
+        else
+          logErrorAndThrow ref ("explicit parameter '" ++ n ++ "' is missing, unused named arguments " ++ toString (namedArgs.map $ fun narg => narg.name))
+      };
+      if explicit then
+        processExplictArg ()
+      else match c.binderInfo with
+        | BinderInfo.implicit => do
+          a ← mkFreshExprMVar d;
+          elabAppArgsAux argIdx namedArgs instMVars (b.instantiate1 a) (mkApp e a)
+        | BinderInfo.instImplicit => do
+          a ← mkFreshExprMVar d true;
+          let mvarId := a.mvarId!;
+          registerSyntheticMVar mvarId ref SyntheticMVarKind.typeClass;
+          elabAppArgsAux argIdx namedArgs (instMVars.push mvarId) (b.instantiate1 a) (mkApp e a)
+        | _ =>
          processExplictArg ()
-        else match c.binderInfo with
-          | BinderInfo.implicit => do
-            a ← mkFreshExprMVar d;
-            elabAppArgsAux argIdx namedArgs (b.instantiate1 a) (mkApp e a)
-          | BinderInfo.instImplicit =>
-            -- TODO
-            pure e
-          | _ =>
-            processExplictArg ()
-    | _ =>
+  | _ =>
+    if namedArgs.isEmpty && argIdx == args.size then
+      finalize ()
+    else
      -- TODO: try `HasCoeToFun`
      logErrorAndThrow ref "too many arguments"

 private def elabAppArgs (ref : Syntax) (f : Expr) (namedArgs : Array NamedArg) (args : Array Syntax)
    (expectedType? : Option Expr) (explicit : Bool) : TermElabM Expr := do
 fType ← inferType f;
-elabAppArgsAux ref args expectedType? explicit 0 namedArgs fType f
+let argIdx    := 0;
+let instMVars := #[];
+elabAppArgsAux ref args expectedType? explicit argIdx namedArgs instMVars fType f

 private def elabAppProjs (ref : Syntax) (f : Expr) (projs : List String) (namedArgs : Array NamedArg) (args : Array Syntax)
    (expectedType? : Option Expr) (explicit : Bool) : TermElabM Expr :=
--- a/stage0/src/Init/Lean/Parser/Parser.lean
+++ b/stage0/src/Init/Lean/Parser/Parser.lean
@ -1589,6 +1589,13 @@ Id.run (s.foldSepArgsM f b)
@[inline] def forSepArgsM (s : Syntax) (f : Syntax → m Unit) : m Unit :=
 s.foldSepArgsM (fun s _ => f s) ()

+@[inline] def foldSepRevArgsM (s : Syntax) (f : Syntax → β → m β) (b : β) : m β := do
+let args := foldSepArgs s (fun arg (args : Array Syntax) => args.push arg) #[];
+args.foldrM f b
+
+@[inline] def foldSepRevArgs (s : Syntax) (f : Syntax → β → β) (b : β) : β := do
+Id.run $ foldSepRevArgsM s f b
+
 end

 end Syntax
--- a/stage0/src/Init/Lean/Parser/Term.lean
+++ b/stage0/src/Init/Lean/Parser/Term.lean
@ -169,7 +169,7 @@ def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Te
@[builtinTermParser] def orM         := tparser! infixR " <||> " 30
@[builtinTermParser] def andM        := tparser! infixR " <&&> " 35
@[builtinTermParser] def andthen     := tparser! infixR " >> "  60
-@[builtinTermParser] def bind        := tparser! infixR " >>= " 55
+@[builtinTermParser] def bindOp      := tparser! infixR " >>= " 55
@[builtinTermParser] def mapRev      := tparser! infixR " <&> " 100
@[builtinTermParser] def seq         := tparser! infixL " <*> " 60
@[builtinTermParser] def seqLeft     := tparser! infixL " <* "  60
--- a/stage0/src/Init/Lean/Syntax.lean
+++ b/stage0/src/Init/Lean/Syntax.lean
@ -331,11 +331,11 @@ Syntax.node nullKind args
 def mkAtom (val : String) : Syntax :=
 Syntax.atom none val

-@[inline] def mkNode (k : SyntaxNodeKind) (args : List Syntax) : Syntax :=
-Syntax.node k args.toArray
+@[inline] def mkNode (k : SyntaxNodeKind) (args : Array Syntax) : Syntax :=
+Syntax.node k args

-@[inline] def mkNullNode (args : List Syntax) : Syntax :=
-Syntax.node nullKind args.toArray
+@[inline] def mkNullNode (args : Array Syntax := #[]) : Syntax :=
+Syntax.node nullKind args

 def mkOptionalNode (arg : Option Syntax) : Syntax :=
 match arg with
--- a/stage0/stdlib/CMakeLists.txt
+++ b/stage0/stdlib/CMakeLists.txt
--- a/stage0/stdlib/Init/Data/Fin/Basic.c
+++ b/stage0/stdlib/Init/Data/Fin/Basic.c
@ -23,7 +23,6 @@ lean_object* l_Fin_DecidableEq(lean_object*);
 uint8_t l_Fin_decLe___rarg(lean_object*, lean_object*);
 lean_object* l_Fin_HasOne(lean_object*);
 lean_object* l_Fin_land___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* l_Fin_HasModn(lean_object*);
 lean_object* l_Fin_HasLessEq(lean_object*);
 lean_object* l_Fin_div(lean_object*, lean_object*, lean_object*);
 lean_object* l_Fin_add___boxed(lean_object*, lean_object*, lean_object*);
@ -52,6 +51,7 @@ lean_object* l_Fin_HasLess___boxed(lean_object*);
 lean_object* l_Fin_mod___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Fin_decLt(lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
+lean_object* l_Fin_HasModN(lean_object*);
 uint8_t l_Fin_DecidableEq___rarg(lean_object*, lean_object*);
 lean_object* l_Fin_lor(lean_object*, lean_object*, lean_object*);
 lean_object* l_Fin_HasLess(lean_object*);
@ -477,7 +477,7 @@ lean_closure_set(x_2, 0, x_1);
 return x_2;
 }
 }
-lean_object* l_Fin_HasModn(lean_object* x_1) {
+lean_object* l_Fin_HasModN(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
--- a/stage0/stdlib/Init/Data/UInt.c
+++ b/stage0/stdlib/Init/Data/UInt.c
@ -51,7 +51,6 @@ size_t l_USize_sub(size_t, size_t);
 lean_object* l_UInt8_lor___boxed(lean_object*, lean_object*);
 lean_object* l_UInt8_decLe___boxed(lean_object*, lean_object*);
 lean_object* l_UInt64_DecidableEq___boxed(lean_object*, lean_object*);
-lean_object* l_UInt16_HasModn;
 uint32_t l_UInt32_land(uint32_t, uint32_t);
 lean_object* l_UInt16_HasSub___closed__1;
 lean_object* l_UInt32_land___boxed(lean_object*, lean_object*);
@ -69,7 +68,6 @@ lean_object* l_UInt32_mul___boxed(lean_object*, lean_object*);
 lean_object* l_UInt8_HasLess;
 lean_object* l_USize_land___boxed(lean_object*, lean_object*);
 lean_object* l_UInt64_land___boxed(lean_object*, lean_object*);
-lean_object* l_UInt32_HasModn;
 lean_object* l_UInt8_HasDiv___closed__1;
 lean_object* l_UInt16_decLe___boxed(lean_object*, lean_object*);
 lean_object* l_UInt16_HasLessEq;
@ -80,6 +78,7 @@ lean_object* l_uint64Sz___closed__1;
 uint8_t l_UInt8_div(uint8_t, uint8_t);
 uint64_t l_UInt64_HasOne;
 lean_object* l_USize_HasAdd;
+lean_object* l_USize_HasModN;
 uint8_t l_UInt8_Inhabited;
 uint32_t lean_uint32_of_nat(lean_object*);
 uint8_t l_USize_decLt(size_t, size_t);
@ -93,6 +92,7 @@ uint8_t l_UInt8_add(uint8_t, uint8_t);
 uint16_t l_UInt16_add(uint16_t, uint16_t);
 uint8_t l_UInt16_hasDecidableLt(uint16_t, uint16_t);
 lean_object* l_USize_div___boxed(lean_object*, lean_object*);
+lean_object* l_UInt32_HasModN;
 lean_object* l_USize_decEq___boxed(lean_object*, lean_object*);
 lean_object* l_UInt8_ofNat___boxed(lean_object*);
 uint32_t l_UInt32_add(uint32_t, uint32_t);
@ -155,10 +155,10 @@ uint64_t l_UInt64_land(uint64_t, uint64_t);
 uint8_t l_UInt32_hasDecidableLe(uint32_t, uint32_t);
 uint16_t l_UInt16_div(uint16_t, uint16_t);
 uint8_t l_UInt8_land(uint8_t, uint8_t);
-lean_object* l_UInt64_HasModn;
 uint8_t l_UInt32_hasDecidableLt(uint32_t, uint32_t);
 size_t lean_usize_of_nat(lean_object*);
 lean_object* l_UInt64_shiftLeft___boxed(lean_object*, lean_object*);
+lean_object* l_UInt8_HasModN;
 lean_object* l_UInt16_HasMul;
 lean_object* l_UInt32_div___boxed(lean_object*, lean_object*);
 lean_object* l_USize_hasDecidableLt___boxed(lean_object*, lean_object*);
@ -175,15 +175,14 @@ uint8_t l_UInt8_sub(uint8_t, uint8_t);
 lean_object* l_UInt64_HasAdd___closed__1;
 lean_object* l_Nat_toUInt64___boxed(lean_object*);
 lean_object* l_UInt32_DecidableEq___boxed(lean_object*, lean_object*);
+lean_object* l_USize_HasModN___closed__1;
 lean_object* l_UInt32_HasSub___closed__1;
 uint8_t l_UInt32_decEq(uint32_t, uint32_t);
 lean_object* l_UInt16_HasAdd;
-lean_object* l_USize_HasModn;
 lean_object* l_USize_HasMul___closed__1;
 uint16_t l_UInt16_Inhabited;
 lean_object* l_USize_modn___boxed(lean_object*, lean_object*);
 uint8_t l_UInt8_HasOne;
-lean_object* l_USize_HasModn___closed__1;
 lean_object* l_USize_DecidableEq___boxed(lean_object*, lean_object*);
 uint8_t l_UInt64_toUInt8(uint64_t);
 lean_object* l_UInt8_HasSub___closed__1;
@ -193,8 +192,8 @@ lean_object* l_UInt32_mod___boxed(lean_object*, lean_object*);
 lean_object* l_usizeSz___closed__1;
 uint64_t lean_uint64_modn(uint64_t, lean_object*);
 uint8_t l_UInt64_DecidableEq(uint64_t, uint64_t);
+lean_object* l_UInt16_HasModN;
 uint32_t l_UInt32_Inhabited;
-lean_object* l_UInt64_HasModn___closed__1;
 lean_object* l_UInt32_HasAdd;
 lean_object* l_Bool_toUInt64___boxed(lean_object*);
 uint32_t l_USize_toUInt32(size_t);
@ -205,11 +204,11 @@ lean_object* l_UInt64_toNat___boxed(lean_object*);
 lean_object* l_UInt16_toNat___boxed(lean_object*);
 lean_object* l_USize_HasLessEq;
 uint64_t l_UInt64_lor(uint64_t, uint64_t);
+lean_object* l_UInt8_HasModN___closed__1;
 lean_object* l_UInt16_hasDecidableLe___boxed(lean_object*, lean_object*);
 lean_object* l_UInt32_HasSub;
 uint8_t l_UInt16_decLt(uint16_t, uint16_t);
 lean_object* l_UInt32_ofNat___boxed(lean_object*);
-lean_object* l_UInt8_HasModn;
 lean_object* l_UInt64_HasLess;
 lean_object* l_UInt64_HasMod___closed__1;
 uint64_t l_UInt64_HasZero;
@ -245,7 +244,6 @@ lean_object* l_Nat_toUInt32___boxed(lean_object*);
 lean_object* l_UInt8_DecidableEq___boxed(lean_object*, lean_object*);
 lean_object* l_USize_HasDiv;
 lean_object* lean_uint64_to_nat(uint64_t);
-lean_object* l_UInt8_HasModn___closed__1;
 lean_object* l_UInt16_mod___boxed(lean_object*, lean_object*);
 size_t l_USize_HasZero;
 lean_object* l_USize_toUInt32___boxed(lean_object*);
@ -269,21 +267,23 @@ lean_object* l_Nat_toUInt8___boxed(lean_object*);
 uint16_t l_UInt64_toUInt16(uint64_t);
 lean_object* l_UInt64_mod___boxed(lean_object*, lean_object*);
 uint64_t l_UInt64_sub(uint64_t, uint64_t);
+lean_object* l_UInt32_HasModN___closed__1;
 lean_object* l_UInt32_toUSize___boxed(lean_object*);
 lean_object* lean_uint16_to_nat(uint16_t);
 uint64_t l_UInt64_div(uint64_t, uint64_t);
 uint64_t l_UInt64_shiftRight(uint64_t, uint64_t);
 lean_object* l_UInt32_toUInt64___boxed(lean_object*);
+lean_object* l_UInt64_HasModN;
 uint8_t l_UInt8_mod(uint8_t, uint8_t);
 lean_object* lean_usize_to_nat(size_t);
+lean_object* l_UInt64_HasModN___closed__1;
 uint8_t l_UInt16_decLe(uint16_t, uint16_t);
 uint8_t l_UInt32_decLe(uint32_t, uint32_t);
-lean_object* l_UInt16_HasModn___closed__1;
+lean_object* l_UInt16_HasModN___closed__1;
 lean_object* l_UInt16_HasLess;
 lean_object* lean_uint32_to_nat(uint32_t);
 lean_object* l_UInt64_HasDiv;
 uint8_t l_UInt64_hasDecidableLe(uint64_t, uint64_t);
-lean_object* l_UInt32_HasModn___closed__1;
 lean_object* l_UInt8_HasMul;
 lean_object* l_UInt64_hasDecidableLt___boxed(lean_object*, lean_object*);
 lean_object* l_UInt8_decEq___boxed(lean_object*, lean_object*);
@ -530,7 +530,7 @@ x_1 = l_UInt8_HasMod___closed__1;
 return x_1;
 }
 }
-lean_object* _init_l_UInt8_HasModn___closed__1() {
+lean_object* _init_l_UInt8_HasModN___closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -538,11 +538,11 @@ x_1 = lean_alloc_closure((void*)(l_UInt8_modn___boxed), 2, 0);
 return x_1;
 }
 }
-lean_object* _init_l_UInt8_HasModn() {
+lean_object* _init_l_UInt8_HasModN() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_UInt8_HasModn___closed__1;
+x_1 = l_UInt8_HasModN___closed__1;
 return x_1;
 }
 }
@ -917,7 +917,7 @@ x_1 = l_UInt16_HasMod___closed__1;
 return x_1;
 }
 }
-lean_object* _init_l_UInt16_HasModn___closed__1() {
+lean_object* _init_l_UInt16_HasModN___closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -925,11 +925,11 @@ x_1 = lean_alloc_closure((void*)(l_UInt16_modn___boxed), 2, 0);
 return x_1;
 }
 }
-lean_object* _init_l_UInt16_HasModn() {
+lean_object* _init_l_UInt16_HasModN() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_UInt16_HasModn___closed__1;
+x_1 = l_UInt16_HasModN___closed__1;
 return x_1;
 }
 }
@ -1304,7 +1304,7 @@ x_1 = l_UInt32_HasMod___closed__1;
 return x_1;
 }
 }
-lean_object* _init_l_UInt32_HasModn___closed__1() {
+lean_object* _init_l_UInt32_HasModN___closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -1312,11 +1312,11 @@ x_1 = lean_alloc_closure((void*)(l_UInt32_modn___boxed), 2, 0);
 return x_1;
 }
 }
-lean_object* _init_l_UInt32_HasModn() {
+lean_object* _init_l_UInt32_HasModN() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_UInt32_HasModn___closed__1;
+x_1 = l_UInt32_HasModN___closed__1;
 return x_1;
 }
 }
@ -1769,7 +1769,7 @@ x_1 = l_UInt64_HasMod___closed__1;
 return x_1;
 }
 }
-lean_object* _init_l_UInt64_HasModn___closed__1() {
+lean_object* _init_l_UInt64_HasModN___closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -1777,11 +1777,11 @@ x_1 = lean_alloc_closure((void*)(l_UInt64_modn___boxed), 2, 0);
 return x_1;
 }
 }
-lean_object* _init_l_UInt64_HasModn() {
+lean_object* _init_l_UInt64_HasModN() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_UInt64_HasModn___closed__1;
+x_1 = l_UInt64_HasModN___closed__1;
 return x_1;
 }
 }
@ -2236,7 +2236,7 @@ x_1 = l_USize_HasMod___closed__1;
 return x_1;
 }
 }
-lean_object* _init_l_USize_HasModn___closed__1() {
+lean_object* _init_l_USize_HasModN___closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -2244,11 +2244,11 @@ x_1 = lean_alloc_closure((void*)(l_USize_modn___boxed), 2, 0);
 return x_1;
 }
 }
-lean_object* _init_l_USize_HasModn() {
+lean_object* _init_l_USize_HasModN() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_USize_HasModn___closed__1;
+x_1 = l_USize_HasModN___closed__1;
 return x_1;
 }
 }
@ -2427,10 +2427,10 @@ l_UInt8_HasMod___closed__1 = _init_l_UInt8_HasMod___closed__1();
 lean_mark_persistent(l_UInt8_HasMod___closed__1);
 l_UInt8_HasMod = _init_l_UInt8_HasMod();
 lean_mark_persistent(l_UInt8_HasMod);
-l_UInt8_HasModn___closed__1 = _init_l_UInt8_HasModn___closed__1();
-lean_mark_persistent(l_UInt8_HasModn___closed__1);
-l_UInt8_HasModn = _init_l_UInt8_HasModn();
-lean_mark_persistent(l_UInt8_HasModn);
+l_UInt8_HasModN___closed__1 = _init_l_UInt8_HasModN___closed__1();
+lean_mark_persistent(l_UInt8_HasModN___closed__1);
+l_UInt8_HasModN = _init_l_UInt8_HasModN();
+lean_mark_persistent(l_UInt8_HasModN);
 l_UInt8_HasDiv___closed__1 = _init_l_UInt8_HasDiv___closed__1();
 lean_mark_persistent(l_UInt8_HasDiv___closed__1);
 l_UInt8_HasDiv = _init_l_UInt8_HasDiv();
@ -2460,10 +2460,10 @@ l_UInt16_HasMod___closed__1 = _init_l_UInt16_HasMod___closed__1();
 lean_mark_persistent(l_UInt16_HasMod___closed__1);
 l_UInt16_HasMod = _init_l_UInt16_HasMod();
 lean_mark_persistent(l_UInt16_HasMod);
-l_UInt16_HasModn___closed__1 = _init_l_UInt16_HasModn___closed__1();
-lean_mark_persistent(l_UInt16_HasModn___closed__1);
-l_UInt16_HasModn = _init_l_UInt16_HasModn();
-lean_mark_persistent(l_UInt16_HasModn);
+l_UInt16_HasModN___closed__1 = _init_l_UInt16_HasModN___closed__1();
+lean_mark_persistent(l_UInt16_HasModN___closed__1);
+l_UInt16_HasModN = _init_l_UInt16_HasModN();
+lean_mark_persistent(l_UInt16_HasModN);
 l_UInt16_HasDiv___closed__1 = _init_l_UInt16_HasDiv___closed__1();
 lean_mark_persistent(l_UInt16_HasDiv___closed__1);
 l_UInt16_HasDiv = _init_l_UInt16_HasDiv();
@ -2493,10 +2493,10 @@ l_UInt32_HasMod___closed__1 = _init_l_UInt32_HasMod___closed__1();
 lean_mark_persistent(l_UInt32_HasMod___closed__1);
 l_UInt32_HasMod = _init_l_UInt32_HasMod();
 lean_mark_persistent(l_UInt32_HasMod);
-l_UInt32_HasModn___closed__1 = _init_l_UInt32_HasModn___closed__1();
-lean_mark_persistent(l_UInt32_HasModn___closed__1);
-l_UInt32_HasModn = _init_l_UInt32_HasModn();
-lean_mark_persistent(l_UInt32_HasModn);
+l_UInt32_HasModN___closed__1 = _init_l_UInt32_HasModN___closed__1();
+lean_mark_persistent(l_UInt32_HasModN___closed__1);
+l_UInt32_HasModN = _init_l_UInt32_HasModN();
+lean_mark_persistent(l_UInt32_HasModN);
 l_UInt32_HasDiv___closed__1 = _init_l_UInt32_HasDiv___closed__1();
 lean_mark_persistent(l_UInt32_HasDiv___closed__1);
 l_UInt32_HasDiv = _init_l_UInt32_HasDiv();
@ -2528,10 +2528,10 @@ l_UInt64_HasMod___closed__1 = _init_l_UInt64_HasMod___closed__1();
 lean_mark_persistent(l_UInt64_HasMod___closed__1);
 l_UInt64_HasMod = _init_l_UInt64_HasMod();
 lean_mark_persistent(l_UInt64_HasMod);
-l_UInt64_HasModn___closed__1 = _init_l_UInt64_HasModn___closed__1();
-lean_mark_persistent(l_UInt64_HasModn___closed__1);
-l_UInt64_HasModn = _init_l_UInt64_HasModn();
-lean_mark_persistent(l_UInt64_HasModn);
+l_UInt64_HasModN___closed__1 = _init_l_UInt64_HasModN___closed__1();
+lean_mark_persistent(l_UInt64_HasModN___closed__1);
+l_UInt64_HasModN = _init_l_UInt64_HasModN();
+lean_mark_persistent(l_UInt64_HasModN);
 l_UInt64_HasDiv___closed__1 = _init_l_UInt64_HasDiv___closed__1();
 lean_mark_persistent(l_UInt64_HasDiv___closed__1);
 l_UInt64_HasDiv = _init_l_UInt64_HasDiv();
@ -2563,10 +2563,10 @@ l_USize_HasMod___closed__1 = _init_l_USize_HasMod___closed__1();
 lean_mark_persistent(l_USize_HasMod___closed__1);
 l_USize_HasMod = _init_l_USize_HasMod();
 lean_mark_persistent(l_USize_HasMod);
-l_USize_HasModn___closed__1 = _init_l_USize_HasModn___closed__1();
-lean_mark_persistent(l_USize_HasModn___closed__1);
-l_USize_HasModn = _init_l_USize_HasModn();
-lean_mark_persistent(l_USize_HasModn);
+l_USize_HasModN___closed__1 = _init_l_USize_HasModN___closed__1();
+lean_mark_persistent(l_USize_HasModN___closed__1);
+l_USize_HasModN = _init_l_USize_HasModN();
+lean_mark_persistent(l_USize_HasModN);
 l_USize_HasDiv___closed__1 = _init_l_USize_HasDiv___closed__1();
 lean_mark_persistent(l_USize_HasDiv___closed__1);
 l_USize_HasDiv = _init_l_USize_HasDiv();
--- a/stage0/stdlib/Init/Lean/Elab.c
+++ b/stage0/stdlib/Init/Lean/Elab.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Elab
-// Imports: Init.Lean.Elab.Import Init.Lean.Elab.Exception Init.Lean.Elab.ElabStrategyAttrs Init.Lean.Elab.Command Init.Lean.Elab.Term Init.Lean.Elab.Frontend
+// Imports: Init.Lean.Elab.Import Init.Lean.Elab.Exception Init.Lean.Elab.ElabStrategyAttrs Init.Lean.Elab.Command Init.Lean.Elab.Term Init.Lean.Elab.Frontend Init.Lean.Elab.BuiltinNotation
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -19,6 +19,7 @@ lean_object* initialize_Init_Lean_Elab_ElabStrategyAttrs(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Command(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Term(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Frontend(lean_object*);
+lean_object* initialize_Init_Lean_Elab_BuiltinNotation(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean_Elab(lean_object* w) {
 lean_object * res;
@ -42,6 +43,9 @@ lean_dec_ref(res);
 res = initialize_Init_Lean_Elab_Frontend(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Elab_BuiltinNotation(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus
--- a/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
+++ b/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
--- a/stage0/stdlib/Init/Lean/Elab/Term.c
+++ b/stage0/stdlib/Init/Lean/Elab/Term.c
--- a/stage0/stdlib/Init/Lean/Parser/Parser.c
+++ b/stage0/stdlib/Init/Lean/Parser/Parser.c
@ -48,6 +48,7 @@ lean_object* l_Lean_Parser_unicodeSymbolInfo___elambda__1___boxed(lean_object*);
 lean_object* l_Lean_Parser_prattParser(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_rawFn___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_andthenInfo(lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_foldSepRevArgs___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Init_Lean_Compiler_InitAttr_2__isUnitType___closed__1;
 extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
 lean_object* l_Lean_Parser_ParserState_mkError(lean_object*, lean_object*);
@ -66,6 +67,7 @@ lean_object* l_Lean_Parser_orelseFn___rarg(lean_object*, lean_object*, lean_obje
 lean_object* l_RBNode_find___main___at_Lean_Parser_TokenMap_insert___spec__1___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_decimalNumberFn___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_nameToExprAux___main___closed__1;
+lean_object* l_Lean_Syntax_foldSepRevArgsM(lean_object*, lean_object*);
 extern lean_object* l_Lean_nullKind;
 lean_object* l_Lean_Parser_andthenAux(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_unicodeSymbolCheckPrecFnAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -86,6 +88,7 @@ lean_object* l_Lean_Parser_registerBuiltinParserAttribute___lambda__1___closed__
 lean_object* l_Lean_Parser_ParserFn_inhabited___rarg(lean_object*);
 lean_object* l_Lean_Parser_binNumberFn___closed__1;
 lean_object* l_Lean_Parser_hexNumberFn___closed__1;
+lean_object* l_Lean_Syntax_foldSepRevArgs(lean_object*);
 lean_object* l_Lean_Parser_binNumberFn___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_many___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_numberFnAux(lean_object*, lean_object*);
@ -214,6 +217,7 @@ lean_object* l_Lean_Syntax_foldSepArgsM___boxed(lean_object*, lean_object*);
 lean_object* lean_string_utf8_byte_size(lean_object*);
 lean_object* l_Lean_Syntax_forSepArgsM(lean_object*);
 lean_object* l_Lean_Parser_ParserState_mkErrorsAt(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_foldSepRevArgs___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_leadingParser(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_symbolNoWsInfo___elambda__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_strLitFn___rarg___closed__1;
@ -252,6 +256,7 @@ lean_object* l_Lean_Parser_unicodeSymbolCheckPrecFn___closed__2;
 lean_object* l_Lean_Parser_quotedSymbolFn___rarg___closed__5;
 lean_object* l_Lean_Parser_optional(uint8_t, lean_object*);
 extern lean_object* l_Lean_AttributeImpl_inhabited___closed__4;
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgs___spec__1(lean_object*);
 lean_object* l_Lean_Parser_mkParserContextCore___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_numLit___boxed(lean_object*);
 lean_object* l_Lean_Parser_insertToken___closed__3;
@ -344,7 +349,9 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_ParserState_keepLatest(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_checkLeadingFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_declareBuiltinParser(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_foldSepRevArgsM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_TokenMap_HasEmptyc(lean_object*);
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgs___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_checkNoWsBefore(uint8_t, lean_object*);
 extern lean_object* l_Lean_choiceKind___closed__2;
 lean_object* l_Lean_Parser_checkWsBefore___boxed(lean_object*, lean_object*);
@ -500,6 +507,7 @@ lean_object* l_Lean_Parser_epsilonInfo___elambda__1___boxed(lean_object*);
 lean_object* l_Lean_Parser_ParserAttribute_inhabited___closed__2;
 lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
 lean_object* l_HashMapImp_insert___at_Lean_Parser_nodeInfo___elambda__1___spec__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Syntax_foldSepRevArgsM___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_mkAtomicInfo___elambda__1(lean_object*);
 lean_object* l_Lean_Parser_anyOfFn(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_AssocList_foldlM___main___at_Lean_Parser_nodeInfo___elambda__1___spec__5(lean_object*, lean_object*);
@ -552,6 +560,7 @@ lean_object* l_Lean_Parser_addBuiltinLeadingParser(lean_object*, lean_object*, l
 lean_object* l_Lean_Parser_mkBuiltinParsingTablesRef(lean_object*);
 lean_object* l_Lean_Syntax_foldSepArgsM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_foldArgsAuxM___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_List_eraseDupsAux___main___at_Lean_Parser_addBuiltinLeadingParser___spec__3(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__2;
 lean_object* l_Lean_ParametricAttribute_setParam___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -588,10 +597,12 @@ lean_object* l_Lean_Parser_ParserState_mkErrorAt(lean_object*, lean_object*, lea
 lean_object* l_Lean_Parser_fieldIdxFn___closed__1;
 lean_object* l_Lean_Parser_Error_HasToString;
 lean_object* l_Lean_Parser_trailingLoop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_symbol___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_checkNoWsBefore___boxed(lean_object*, lean_object*);
 uint8_t l_UInt32_decEq(uint32_t, uint32_t);
 lean_object* l_Lean_Parser_unquotedSymbolFn(uint8_t, lean_object*);
+lean_object* l_Lean_Syntax_foldSepRevArgsM___boxed(lean_object*, lean_object*);
 lean_object* l_String_intercalate(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
 lean_object* l_Lean_Parser_numLit(uint8_t);
@ -704,6 +715,7 @@ lean_object* l_Lean_Parser_chFn___rarg(uint32_t, uint8_t, lean_object*, lean_obj
 lean_object* l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Syntax_forArgsM___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_epsilonInfo___closed__2;
 lean_object* l_Lean_Parser_Parser_inhabited___closed__2;
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_rawCh___elambda__1___boxed(lean_object*);
 lean_object* l_Lean_Parser_numberFnAux___closed__1;
 lean_object* l_Lean_Syntax_forSepArgsM___boxed(lean_object*);
@ -741,6 +753,7 @@ uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_ParserState_mkLongestNodeAlt(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_isNone___boxed(lean_object*);
+lean_object* l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Syntax_foldSepRevArgsM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_currLbp(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_takeWhile1Fn(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_io_initializing(lean_object*);
@ -774,6 +787,7 @@ lean_object* l_Lean_Parser_manyFn(uint8_t, lean_object*, lean_object*, lean_obje
 lean_object* l_Lean_Parser_ParserState_next___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Parser_inhabited___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_chFn___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_sepBy1Info___elambda__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_epsilonInfo___elambda__2(lean_object*);
 lean_object* l___private_Init_Lean_Parser_Parser_1__expectedToString(lean_object*);
@ -870,6 +884,7 @@ lean_object* l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_decimalNumberFn__
 lean_object* l_RBNode_ins___main___at_Lean_Parser_TokenMap_insert___spec__3(lean_object*);
 lean_object* l_Lean_Parser_TokenConfig_HasBeq;
 lean_object* l_Lean_Parser_Parser_inhabited___boxed(lean_object*);
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgs___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_strLitFnAux___main___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkErrorStringWithPos(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_unicodeSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -29438,6 +29453,222 @@ lean_dec(x_1);
 return x_2;
 }
 }
+lean_object* l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Syntax_foldSepRevArgsM___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; uint8_t x_6; 
+x_5 = lean_array_get_size(x_2);
+x_6 = lean_nat_dec_lt(x_3, x_5);
+lean_dec(x_5);
+if (x_6 == 0)
+{
+lean_dec(x_3);
+return x_4;
+}
+else
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_7 = lean_array_fget(x_2, x_3);
+x_8 = lean_array_push(x_4, x_7);
+x_9 = lean_nat_add(x_3, x_1);
+lean_dec(x_3);
+x_3 = x_9;
+x_4 = x_8;
+goto _start;
+}
+}
+}
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2___rarg(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) {
+_start:
+{
+lean_object* x_8; uint8_t x_9; 
+x_8 = lean_unsigned_to_nat(0u);
+x_9 = lean_nat_dec_eq(x_5, x_8);
+if (x_9 == 0)
+{
+lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
+x_10 = lean_unsigned_to_nat(1u);
+x_11 = lean_nat_sub(x_5, x_10);
+x_12 = lean_ctor_get(x_1, 1);
+lean_inc(x_12);
+x_13 = lean_array_fget(x_4, x_11);
+lean_inc(x_3);
+x_14 = lean_apply_2(x_3, x_13, x_7);
+x_15 = lean_alloc_closure((void*)(l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2___rarg___boxed), 7, 6);
+lean_closure_set(x_15, 0, x_1);
+lean_closure_set(x_15, 1, x_2);
+lean_closure_set(x_15, 2, x_3);
+lean_closure_set(x_15, 3, x_4);
+lean_closure_set(x_15, 4, x_11);
+lean_closure_set(x_15, 5, lean_box(0));
+x_16 = lean_apply_4(x_12, lean_box(0), lean_box(0), x_14, x_15);
+return x_16;
+}
+else
+{
+lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_17 = lean_ctor_get(x_1, 0);
+lean_inc(x_17);
+lean_dec(x_1);
+x_18 = lean_ctor_get(x_17, 1);
+lean_inc(x_18);
+lean_dec(x_17);
+x_19 = lean_apply_2(x_18, lean_box(0), x_7);
+return x_19;
+}
+}
+}
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_closure((void*)(l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2___rarg___boxed), 7, 0);
+return x_3;
+}
+}
+lean_object* l_Lean_Syntax_foldSepRevArgsM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_5 = l_Lean_Syntax_getArgs(x_2);
+x_6 = lean_unsigned_to_nat(2u);
+x_7 = lean_unsigned_to_nat(0u);
+x_8 = l_Array_empty___closed__1;
+x_9 = l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Syntax_foldSepRevArgsM___spec__1(x_6, x_5, x_7, x_8);
+lean_dec(x_5);
+x_10 = lean_array_get_size(x_9);
+x_11 = l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2___rarg(x_1, x_2, x_3, x_9, x_10, lean_box(0), x_4);
+lean_dec(x_10);
+return x_11;
+}
+}
+lean_object* l_Lean_Syntax_foldSepRevArgsM(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_closure((void*)(l_Lean_Syntax_foldSepRevArgsM___rarg), 4, 0);
+return x_3;
+}
+}
+lean_object* l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Syntax_foldSepRevArgsM___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Syntax_foldSepRevArgsM___spec__1(x_1, x_2, x_3, x_4);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_5;
+}
+}
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2___rarg___boxed(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) {
+_start:
+{
+lean_object* x_8; 
+x_8 = l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
+lean_dec(x_5);
+return x_8;
+}
+}
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2(x_1, x_2);
+lean_dec(x_2);
+return x_3;
+}
+}
+lean_object* l_Lean_Syntax_foldSepRevArgsM___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Syntax_foldSepRevArgsM(x_1, x_2);
+lean_dec(x_2);
+return x_3;
+}
+}
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgs___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; uint8_t x_8; 
+x_7 = lean_unsigned_to_nat(0u);
+x_8 = lean_nat_dec_eq(x_4, x_7);
+if (x_8 == 0)
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_9 = lean_unsigned_to_nat(1u);
+x_10 = lean_nat_sub(x_4, x_9);
+lean_dec(x_4);
+x_11 = lean_array_fget(x_3, x_10);
+lean_inc(x_2);
+x_12 = lean_apply_2(x_2, x_11, x_6);
+x_4 = x_10;
+x_5 = lean_box(0);
+x_6 = x_12;
+goto _start;
+}
+else
+{
+lean_dec(x_4);
+lean_dec(x_2);
+return x_6;
+}
+}
+}
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgs___spec__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgs___spec__1___rarg___boxed), 6, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_Syntax_foldSepRevArgs___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+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* x_10; 
+x_4 = l_Lean_Syntax_getArgs(x_1);
+x_5 = lean_unsigned_to_nat(2u);
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Array_empty___closed__1;
+x_8 = l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Syntax_foldSepRevArgsM___spec__1(x_5, x_4, x_6, x_7);
+lean_dec(x_4);
+x_9 = lean_array_get_size(x_8);
+x_10 = l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgs___spec__1___rarg(x_1, x_2, x_8, x_9, lean_box(0), x_3);
+lean_dec(x_8);
+return x_10;
+}
+}
+lean_object* l_Lean_Syntax_foldSepRevArgs(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Syntax_foldSepRevArgs___rarg___boxed), 3, 0);
+return x_2;
+}
+}
+lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgs___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; 
+x_7 = l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgs___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_3);
+lean_dec(x_1);
+return x_7;
+}
+}
+lean_object* l_Lean_Syntax_foldSepRevArgs___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_Syntax_foldSepRevArgs___rarg(x_1, x_2, x_3);
+lean_dec(x_1);
+return x_4;
+}
+}
 lean_object* initialize_Init_Lean_Data_Trie(lean_object*);
 lean_object* initialize_Init_Lean_Data_Position(lean_object*);
 lean_object* initialize_Init_Lean_Syntax(lean_object*);
--- a/stage0/stdlib/Init/Lean/Parser/Term.c
+++ b/stage0/stdlib/Init/Lean/Parser/Term.c
@ -46,6 +46,7 @@ lean_object* l_Lean_Parser_Term_quotedName___closed__4;
 lean_object* l_Lean_Parser_Term_andthen___elambda__1___closed__2;
 lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_doSeq___elambda__1___spec__2(uint8_t, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_app___elambda__1___closed__1;
+lean_object* l_Lean_Parser_Term_bindOp___elambda__1(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_manyAux___main___closed__1;
 lean_object* l_Lean_Parser_Term_doPat___elambda__1___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__10;
@ -296,7 +297,6 @@ lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Term_letPatDecl___closed__4;
 lean_object* l_Lean_Parser_Term_or___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_quotedName___closed__5;
-lean_object* l_Lean_Parser_Term_bind;
 lean_object* l_Lean_Parser_Term_match__syntax___closed__3;
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_match___elambda__1___spec__1___closed__1;
 extern lean_object* l_Lean_Parser_symbolNoWsFn___closed__1;
@ -510,10 +510,10 @@ lean_object* l_Lean_Parser_Term_ge___closed__1;
 lean_object* l_Lean_Parser_Term_prop___elambda__1___rarg___closed__2;
 lean_object* l_Lean_Parser_Term_arrayRef___closed__5;
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___elambda__1___spec__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Term_bindOp___closed__3;
 lean_object* l_Lean_Parser_Term_add___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_show___elambda__1___rarg___closed__2;
 lean_object* l_Lean_Parser_Term_parser_x21___elambda__1(lean_object*);
-lean_object* l_Lean_Parser_Term_bind___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_match___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_beq___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_bnot___elambda__1___rarg___closed__6;
@ -589,7 +589,6 @@ lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_
 lean_object* l_Lean_Parser_Term_namedPattern;
 lean_object* l_Lean_Parser_Term_seqLeft___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_quotedName___elambda__1___rarg___closed__1;
-lean_object* l_Lean_Parser_Term_bind___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_match___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Term_anonymousCtor___closed__3;
 lean_object* l_Lean_Parser_Term_suffices___elambda__1___rarg___closed__7;
@ -683,7 +682,6 @@ lean_object* l_Lean_Parser_noFirstTokenInfo(lean_object*);
 lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___rarg___closed__1;
 lean_object* l_Lean_Parser_Term_letDecl;
 lean_object* l_Lean_Parser_Term_id___closed__2;
-lean_object* l_Lean_Parser_Term_bind___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Term_emptyC___elambda__1___boxed(lean_object*);
 extern lean_object* l_Lean_Parser_checkLeadingFn___closed__1;
@ -750,7 +748,6 @@ lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___elambd
 lean_object* l_Lean_Parser_Term_bnot;
 lean_object* l_Lean_Parser_Term_doLet___closed__3;
 lean_object* l_Lean_Parser_Term_seq___elambda__1___closed__2;
-lean_object* l_Lean_Parser_Term_bind___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Term_bnot___closed__5;
 lean_object* l_Lean_Parser_Term_paren___closed__4;
 lean_object* l_Lean_Parser_Term_mul;
@ -808,6 +805,7 @@ lean_object* l_Lean_Parser_Term_le___closed__3;
 lean_object* l_Lean_Parser_Term_fcomp;
 lean_object* l_Lean_Parser_Term_depArrow___closed__4;
 lean_object* l_Lean_Parser_Term_subtype___closed__5;
+lean_object* l___regBuiltinParser_Lean_Parser_Term_bindOp(lean_object*);
 lean_object* l_Lean_Parser_Term_doExpr___elambda__1___rarg___closed__2;
 lean_object* l_Lean_Parser_Term_seqRight___closed__2;
 lean_object* l_Lean_Parser_Term_matchAlt___elambda__1___closed__6;
@ -888,6 +886,7 @@ lean_object* l_Lean_Parser_Term_structInstSource___closed__3;
 lean_object* l___regBuiltinParser_Lean_Parser_Term_seq(lean_object*);
 lean_object* l_Lean_Parser_Term_equation;
 lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__3;
+lean_object* l_Lean_Parser_Term_bindOp___closed__2;
 lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___rarg___closed__3;
 extern lean_object* l_Lean_Parser_Level_paren___elambda__1___rarg___closed__12;
 lean_object* l_Lean_Parser_Term_uminus___closed__5;
@ -907,6 +906,7 @@ lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___rarg___closed__7;
 lean_object* l_Lean_Parser_Term_orM___elambda__1___closed__2;
 lean_object* l___regBuiltinParser_Lean_Parser_Term_anonymousCtor(lean_object*);
 lean_object* l_Lean_Parser_Term_lt___closed__1;
+lean_object* l_Lean_Parser_Term_bindOp___closed__1;
 lean_object* l_Lean_Parser_Term_seq;
 lean_object* l_Lean_Parser_Term_depArrow___closed__1;
 lean_object* l_Lean_Parser_Term_bnot___elambda__1___rarg(lean_object*, lean_object*);
@ -1166,7 +1166,6 @@ lean_object* l_Lean_Parser_Term_match__syntax___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Term_beq___closed__3;
 lean_object* l_Lean_Parser_Term_id___closed__1;
 lean_object* l_Lean_Parser_Term_arrayRef___closed__2;
-lean_object* l_Lean_Parser_Term_bind___closed__1;
 lean_object* l_Lean_Parser_Term_stxQuot___closed__5;
 extern lean_object* l_Lean_Parser_appPrec;
 lean_object* l_Lean_Parser_Term_if___elambda__1___rarg___closed__1;
@ -1192,7 +1191,6 @@ lean_object* l_Lean_Parser_Term_arrayLit;
 lean_object* l_Lean_Parser_Term_mul___closed__2;
 lean_object* l_Lean_Parser_Term_mod___closed__2;
 lean_object* l_Lean_Parser_Term_leftArrow;
-lean_object* l_Lean_Parser_Term_bind___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_cdot___elambda__1___rarg___closed__6;
 lean_object* l_Lean_Parser_Term_namedPattern___closed__4;
 lean_object* l_Lean_Parser_Term_seq___elambda__1___closed__3;
@ -1208,6 +1206,7 @@ lean_object* l_Lean_Parser_Term_modN___elambda__1(lean_object*, lean_object*, le
 lean_object* l_Lean_Parser_Term_map___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinParser_Lean_Parser_Term_le(lean_object*);
 lean_object* l_Lean_Parser_Term_seqRight;
+lean_object* l_Lean_Parser_Term_bindOp;
 lean_object* l_Lean_Parser_Term_simpleBinder;
 lean_object* l_Lean_Parser_Term_matchAlt___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_bor___elambda__1___closed__3;
@ -1419,7 +1418,6 @@ lean_object* l_Lean_Parser_Term_arrayRef___closed__1;
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___elambda__1___spec__1___closed__1;
 lean_object* l_Lean_Parser_builtinTermParsingTable;
 lean_object* l_Lean_Parser_Term_fromTerm___closed__5;
-lean_object* l___regBuiltinParser_Lean_Parser_Term_bind(lean_object*);
 lean_object* l_Lean_Parser_Term_doExpr___elambda__1___boxed(lean_object*);
 lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___rarg___closed__7;
 lean_object* l_Lean_Parser_Term_optType___elambda__1___boxed(lean_object*);
@ -1485,6 +1483,7 @@ lean_object* l_String_trim(lean_object*);
 lean_object* l_Lean_Parser_Term_namedArgument___elambda__1___rarg(lean_object*, lean_object*);
 lean_object* l___regBuiltinParser_Lean_Parser_Term_prop(lean_object*);
 lean_object* l___regBuiltinParser_Lean_Parser_Term_antiquot(lean_object*);
+lean_object* l_Lean_Parser_Term_bindOp___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_explicitBinder___closed__9;
 lean_object* l_Lean_Parser_Term_letEqns___closed__4;
 lean_object* l_Lean_Parser_Term_pow___closed__3;
@ -1495,7 +1494,6 @@ lean_object* l_Lean_Parser_Term_if___closed__9;
 lean_object* l_Lean_Parser_Term_doLet___closed__1;
 lean_object* l___regBuiltinParser_Lean_Parser_Term_modN(lean_object*);
 lean_object* l_Lean_Parser_Term_typeSpec___closed__1;
-lean_object* l_Lean_Parser_Term_bind___closed__2;
 lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___rarg___closed__5;
 lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Term_namedArgument___closed__6;
@ -1643,6 +1641,7 @@ lean_object* l_Lean_Parser_unicodeSymbolInfo(lean_object*, lean_object*, lean_ob
 lean_object* l_Lean_Parser_Term_not___elambda__1___rarg___closed__7;
 lean_object* l_Lean_Parser_Term_borrowed___closed__2;
 lean_object* l_Lean_Parser_Term_mapRev___elambda__1___closed__4;
+lean_object* l_Lean_Parser_Term_bindOp___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_suffices;
 lean_object* l_Lean_Parser_Term_mapConstRev;
@ -1674,6 +1673,7 @@ lean_object* l_Lean_Parser_Term_subtype___closed__4;
 lean_object* l_Lean_Parser_Term_nomatch___closed__3;
 lean_object* l_Lean_Parser_Term_orM___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_structInstField___elambda__1___rarg(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Term_bindOp___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_add___closed__3;
 lean_object* l_Lean_Parser_Term_structInst;
 lean_object* l_Lean_Parser_Term_type___elambda__1___boxed(lean_object*);
@ -1712,6 +1712,7 @@ lean_object* l_Lean_Parser_Term_structInst___closed__11;
 lean_object* l_Lean_Parser_Term_mapConstRev___closed__1;
 lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__8;
 lean_object* l_Lean_Parser_charLitFn___rarg(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Term_bindOp___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_borrowed___elambda__1___rarg___closed__1;
 lean_object* l_Lean_Parser_Term_do___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_letDecl___closed__3;
@ -1782,7 +1783,6 @@ lean_object* l_Lean_Parser_Term_not___elambda__1___rarg___closed__5;
 lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Term_letEqns___closed__6;
 extern lean_object* l_Lean_Parser_Level_paren___closed__1;
-lean_object* l_Lean_Parser_Term_bind___closed__3;
 lean_object* l_Lean_Parser_fieldIdxFn(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_arrayRef___closed__3;
 lean_object* l_Lean_Parser_Term_hole___closed__1;
@ -29241,25 +29241,25 @@ x_5 = l_Lean_Parser_addBuiltinTrailingParser(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_bind___elambda__1___closed__1() {
+lean_object* _init_l_Lean_Parser_Term_bindOp___elambda__1___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("bind");
+x_1 = lean_mk_string("bindOp");
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_bind___elambda__1___closed__2() {
+lean_object* _init_l_Lean_Parser_Term_bindOp___elambda__1___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2;
-x_2 = l_Lean_Parser_Term_bind___elambda__1___closed__1;
+x_2 = l_Lean_Parser_Term_bindOp___elambda__1___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_bind___elambda__1___closed__3() {
+lean_object* _init_l_Lean_Parser_Term_bindOp___elambda__1___closed__3() {
 _start:
 {
 lean_object* x_1; 
@ -29267,21 +29267,21 @@ x_1 = lean_mk_string(" >>= ");
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_bind___elambda__1___closed__4() {
+lean_object* _init_l_Lean_Parser_Term_bindOp___elambda__1___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_bind___elambda__1___closed__3;
+x_1 = l_Lean_Parser_Term_bindOp___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(55u);
 x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
-lean_object* l_Lean_Parser_Term_bind___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_Parser_Term_bindOp___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 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* x_10; 
-x_4 = l_Lean_Parser_Term_bind___elambda__1___closed__4;
+x_4 = l_Lean_Parser_Term_bindOp___elambda__1___closed__4;
 x_5 = lean_ctor_get(x_4, 1);
 lean_inc(x_5);
 x_6 = lean_ctor_get(x_3, 0);
@ -29289,58 +29289,58 @@ lean_inc(x_6);
 x_7 = lean_array_get_size(x_6);
 lean_dec(x_6);
 x_8 = lean_apply_3(x_5, x_1, x_2, x_3);
-x_9 = l_Lean_Parser_Term_bind___elambda__1___closed__2;
+x_9 = l_Lean_Parser_Term_bindOp___elambda__1___closed__2;
 x_10 = l_Lean_Parser_ParserState_mkNode(x_8, x_9, x_7);
 return x_10;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_bind___closed__1() {
+lean_object* _init_l_Lean_Parser_Term_bindOp___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Parser_Term_bind___elambda__1___closed__4;
+x_1 = l_Lean_Parser_Term_bindOp___elambda__1___closed__4;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Term_bind___elambda__1___closed__2;
+x_3 = l_Lean_Parser_Term_bindOp___elambda__1___closed__2;
 x_4 = l_Lean_Parser_nodeInfo(x_3, x_2);
 return x_4;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_bind___closed__2() {
+lean_object* _init_l_Lean_Parser_Term_bindOp___closed__2() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_bind___elambda__1), 3, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_bindOp___elambda__1), 3, 0);
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_bind___closed__3() {
+lean_object* _init_l_Lean_Parser_Term_bindOp___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_bind___closed__1;
-x_2 = l_Lean_Parser_Term_bind___closed__2;
+x_1 = l_Lean_Parser_Term_bindOp___closed__1;
+x_2 = l_Lean_Parser_Term_bindOp___closed__2;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_bind() {
+lean_object* _init_l_Lean_Parser_Term_bindOp() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Term_bind___closed__3;
+x_1 = l_Lean_Parser_Term_bindOp___closed__3;
 return x_1;
 }
 }
-lean_object* l___regBuiltinParser_Lean_Parser_Term_bind(lean_object* x_1) {
+lean_object* l___regBuiltinParser_Lean_Parser_Term_bindOp(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_Parser_builtinTermParsingTable;
-x_3 = l_Lean_Parser_Term_bind___elambda__1___closed__2;
-x_4 = l_Lean_Parser_Term_bind;
+x_3 = l_Lean_Parser_Term_bindOp___elambda__1___closed__2;
+x_4 = l_Lean_Parser_Term_bindOp;
 x_5 = l_Lean_Parser_addBuiltinTrailingParser(x_2, x_3, x_4, x_1);
 return x_5;
 }
@ -32833,23 +32833,23 @@ lean_mark_persistent(l_Lean_Parser_Term_andthen);
 res = l___regBuiltinParser_Lean_Parser_Term_andthen(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-l_Lean_Parser_Term_bind___elambda__1___closed__1 = _init_l_Lean_Parser_Term_bind___elambda__1___closed__1();
-lean_mark_persistent(l_Lean_Parser_Term_bind___elambda__1___closed__1);
-l_Lean_Parser_Term_bind___elambda__1___closed__2 = _init_l_Lean_Parser_Term_bind___elambda__1___closed__2();
-lean_mark_persistent(l_Lean_Parser_Term_bind___elambda__1___closed__2);
-l_Lean_Parser_Term_bind___elambda__1___closed__3 = _init_l_Lean_Parser_Term_bind___elambda__1___closed__3();
-lean_mark_persistent(l_Lean_Parser_Term_bind___elambda__1___closed__3);
-l_Lean_Parser_Term_bind___elambda__1___closed__4 = _init_l_Lean_Parser_Term_bind___elambda__1___closed__4();
-lean_mark_persistent(l_Lean_Parser_Term_bind___elambda__1___closed__4);
-l_Lean_Parser_Term_bind___closed__1 = _init_l_Lean_Parser_Term_bind___closed__1();
-lean_mark_persistent(l_Lean_Parser_Term_bind___closed__1);
-l_Lean_Parser_Term_bind___closed__2 = _init_l_Lean_Parser_Term_bind___closed__2();
-lean_mark_persistent(l_Lean_Parser_Term_bind___closed__2);
-l_Lean_Parser_Term_bind___closed__3 = _init_l_Lean_Parser_Term_bind___closed__3();
-lean_mark_persistent(l_Lean_Parser_Term_bind___closed__3);
-l_Lean_Parser_Term_bind = _init_l_Lean_Parser_Term_bind();
-lean_mark_persistent(l_Lean_Parser_Term_bind);
-res = l___regBuiltinParser_Lean_Parser_Term_bind(lean_io_mk_world());
+l_Lean_Parser_Term_bindOp___elambda__1___closed__1 = _init_l_Lean_Parser_Term_bindOp___elambda__1___closed__1();
+lean_mark_persistent(l_Lean_Parser_Term_bindOp___elambda__1___closed__1);
+l_Lean_Parser_Term_bindOp___elambda__1___closed__2 = _init_l_Lean_Parser_Term_bindOp___elambda__1___closed__2();
+lean_mark_persistent(l_Lean_Parser_Term_bindOp___elambda__1___closed__2);
+l_Lean_Parser_Term_bindOp___elambda__1___closed__3 = _init_l_Lean_Parser_Term_bindOp___elambda__1___closed__3();
+lean_mark_persistent(l_Lean_Parser_Term_bindOp___elambda__1___closed__3);
+l_Lean_Parser_Term_bindOp___elambda__1___closed__4 = _init_l_Lean_Parser_Term_bindOp___elambda__1___closed__4();
+lean_mark_persistent(l_Lean_Parser_Term_bindOp___elambda__1___closed__4);
+l_Lean_Parser_Term_bindOp___closed__1 = _init_l_Lean_Parser_Term_bindOp___closed__1();
+lean_mark_persistent(l_Lean_Parser_Term_bindOp___closed__1);
+l_Lean_Parser_Term_bindOp___closed__2 = _init_l_Lean_Parser_Term_bindOp___closed__2();
+lean_mark_persistent(l_Lean_Parser_Term_bindOp___closed__2);
+l_Lean_Parser_Term_bindOp___closed__3 = _init_l_Lean_Parser_Term_bindOp___closed__3();
+lean_mark_persistent(l_Lean_Parser_Term_bindOp___closed__3);
+l_Lean_Parser_Term_bindOp = _init_l_Lean_Parser_Term_bindOp();
+lean_mark_persistent(l_Lean_Parser_Term_bindOp);
+res = l___regBuiltinParser_Lean_Parser_Term_bindOp(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 l_Lean_Parser_Term_mapRev___elambda__1___closed__1 = _init_l_Lean_Parser_Term_mapRev___elambda__1___closed__1();
--- a/stage0/stdlib/Init/Lean/Syntax.c
+++ b/stage0/stdlib/Init/Lean/Syntax.c
@ -152,7 +152,6 @@ lean_object* l_Lean_SyntaxNode_modifyArgs(lean_object*, lean_object*);
 lean_object* l_Lean_SyntaxNode_getArgs___boxed(lean_object*);
 lean_object* l_Lean_unreachIsNodeIdent___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_SourceInfo_appendToLeading(lean_object*, lean_object*);
-lean_object* l_List_redLength___main___rarg(lean_object*);
 lean_object* l_Lean_Syntax_getTailInfo___main___boxed(lean_object*);
 lean_object* l_Lean_nullKind___closed__1;
 lean_object* l_Lean_Syntax_ifNode___rarg(lean_object*, lean_object*, lean_object*);
@ -234,7 +233,6 @@ lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_toNat(lean_object*);
 extern lean_object* l_Lean_Format_paren___closed__3;
 lean_object* l_Lean_Syntax_asNode(lean_object*);
-lean_object* l_List_toArrayAux___main___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_unreachIsNodeIdent(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_System_FilePath_dirName___closed__1;
 lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
@ -4006,30 +4004,22 @@ return x_3;
 lean_object* l_Lean_mkNode(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_3 = l_List_redLength___main___rarg(x_2);
-x_4 = lean_mk_empty_array_with_capacity(x_3);
-lean_dec(x_3);
-x_5 = l_List_toArrayAux___main___rarg(x_2, x_4);
-x_6 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_6, 0, x_1);
-lean_ctor_set(x_6, 1, x_5);
-return x_6;
+lean_object* x_3; 
+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_mkNullNode(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_2 = l_List_redLength___main___rarg(x_1);
-x_3 = lean_mk_empty_array_with_capacity(x_2);
-lean_dec(x_2);
-x_4 = l_List_toArrayAux___main___rarg(x_1, x_3);
-x_5 = l_Lean_nullKind;
-x_6 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_6, 0, x_5);
-lean_ctor_set(x_6, 1, x_4);
-return x_6;
+lean_object* x_2; lean_object* x_3; 
+x_2 = l_Lean_nullKind;
+x_3 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_3, 0, x_2);
+lean_ctor_set(x_3, 1, x_1);
+return x_3;
 }
 }
 lean_object* _init_l_Lean_mkOptionalNode___closed__1() {