chore: update stage0

stage0/src/Init/Core.lean

@@ -279,11 +279,27 @@ inductive ForInStep (α : Type u)
 | yield : α → ForInStep
 
 /- Auxiliary type used to compile `do` notation. -/
-inductive DoResult (α : Type u) (β : Type v)
-| «break»    : β → DoResult
-| «continue» : β → DoResult
-| «return»   : α → β → DoResult
-| «pure»     : α → β → DoResult
+inductive DoResultPRBC (α β σ : Type u)
+| «pure»     : α → σ → DoResultPRBC
+| «return»   : β → σ → DoResultPRBC
+| «break»    : σ → DoResultPRBC
+| «continue» : σ → DoResultPRBC
+
+/- Auxiliary type used to compile `do` notation. -/
+inductive DoResultPR (α β σ : Type u)
+| «pure»     : α → σ → DoResultPR
+| «return»   : β → σ → DoResultPR
+
+/- Auxiliary type used to compile `do` notation. -/
+inductive DoResultBC (σ : Type u)
+| «break»    : σ → DoResultBC
+| «continue» : σ → DoResultBC
+
+/- Auxiliary type used to compile `do` notation. -/
+inductive DoResultSBC (α σ : Type u)
+| «pureReturn» : α → σ → DoResultSBC
+| «break»      : σ → DoResultSBC
+| «continue»   : σ → DoResultSBC
 
 class inductive Decidable (p : Prop)
 | isFalse (h : ¬p) : Decidable

stage0/src/Init/Data/Array.lean

@@ -7,3 +7,4 @@ prelude
 import Init.Data.Array.Basic
 import Init.Data.Array.QSort
 import Init.Data.Array.BinSearch
+import Init.Data.Array.ForIn

stage0/src/Init/Data/Array/ForIn.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Data.Array.Basic
+new_frontend
+
+namespace Array
+universes u v w
+
+/-
+  We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime.
+
+  This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies `as.size < usizeSz` to true. -/
+@[inline] unsafe def forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
+let sz := USize.ofNat as.size
+let rec @[specialize] loop (i : USize) (b : β) : m β := do
+  if i < sz then
+    let a := as.uget i lcProof
+    match (← f a b) with
+    | ForInStep.done  b => pure b
+    | ForInStep.yield b => loop (i+1) b
+  else
+    pure b
+loop 0 b
+
+-- Move?
+private theorem zeroLtOfLt : {a b : Nat} → a < b → 0 < b
+| 0,   _, h => h
+| a+1, b, h =>
+  have a < b from Nat.ltTrans (Nat.ltSuccSelf _) h
+  zeroLtOfLt this
+
+/- Reference implementation for `Array.forIn` -/
+@[implementedBy Array.forInUnsafe]
+def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
+let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
+  match i, h with
+  | 0,   _ => pure b
+  | i+1, h =>
+    have h' : i < as.size          from Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
+    have as.size - 1 < as.size     from Nat.subLt (zeroLtOfLt h') (decide! (0 < 1))
+    have as.size - 1 - i < as.size from Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
+    match (← f (as.get ⟨as.size - 1 - i, this⟩) b) with
+    | ForInStep.done b  => pure b
+    | ForInStep.yield b => loop i (Nat.leOfLt h') b
+loop as.size (Nat.leRefl _) b
+
+end Array

stage0/src/Init/Data/Fin/Basic.lean

@@ -6,12 +6,16 @@ Author: Leonardo de Moura
 prelude
 import Init.Data.Nat.Div
 import Init.Data.Nat.Bitwise
+import Init.Coe
 
 open Nat
 structure Fin (n : Nat) := (val : Nat) (isLt : val < n)
 
 namespace Fin
 
+instance coeToNat {n} : Coe (Fin n) Nat :=
+⟨fun v => v.val⟩
+
 protected def lt {n} (a b : Fin n) : Prop :=
 a.val < b.val
 

stage0/src/Init/LeanInit.lean

@@ -218,6 +218,8 @@ def charLitKind : SyntaxNodeKind := `charLit
 def numLitKind : SyntaxNodeKind := `numLit
 def nameLitKind : SyntaxNodeKind := `nameLit
 def fieldIdxKind : SyntaxNodeKind := `fieldIdx
+def interpolatedStrLitKind : SyntaxNodeKind := `interpolatedStrLitKind
+def interpolatedStrKind : SyntaxNodeKind := `interpolatedStrKind
 
 namespace Syntax
 
@@ -911,3 +913,46 @@ end Array
   Like `optParam`, this gadget only affects elaboration.
   For example, the tactic will *not* be invoked during type class resolution. -/
 abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α
+
+new_frontend
+
+/- Helper functions for manipulating interpolated strings -/
+namespace Lean.Syntax
+
+private def decodeInterpStrQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) :=
+match decodeQuotedChar s i with
+| some r => some r
+| none   =>
+  let c := s.get i
+  let i := s.next i
+  if c == '{' then pure ('{', i)
+  else none
+
+private partial def decodeInterpStrLit (s : String) : Option String :=
+let rec loop (i : String.Pos) (acc : String) :=
+  let c := s.get i
+  let i := s.next i
+  if c == '\"' || c == '{' then
+    pure acc
+  else if s.atEnd i then
+    none
+  else if c == '\\' then do
+    let (c, i) ← decodeInterpStrQuotedChar s i
+    loop i (acc.push c)
+  else
+    loop i (acc.push c)
+loop 1 ""
+
+partial def isInterpolatedStrLit? (stx : Syntax) : Option String :=
+match isLit? interpolatedStrLitKind stx with
+| none     => none
+| some val => decodeInterpStrLit val
+
+def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → Syntax → MacroM Syntax) (mkElem : Syntax → MacroM Syntax) : MacroM Syntax :=
+chunks.iterateM Syntax.missing fun i elem result => do
+  let elem ← match elem.isInterpolatedStrLit? with
+    | none     => mkElem elem
+    | some str => mkElem (mkStxStrLit str)
+  if i.val == 0 then pure elem else mkAppend result elem
+
+end Lean.Syntax

stage0/src/Lean/Elab/Do.lean

@@ -203,14 +203,16 @@ def isTerminalAction : Code → Bool
 def hasTerminalAction (c : Code) : Bool :=
 hasExitPointPred isTerminalAction c
 
+def hasBreakContinue (c : Code) : Bool :=
+hasExitPointPred (fun c => match c with | Code.«break» _ => true | Code.«continue» _ => true | _ => false) c
+
 def hasBreakContinueReturn (c : Code) : Bool :=
 hasExitPointPred (fun c => !isTerminalAction c) c
 
 def mkAuxDeclFor {m} [Monad m] [MonadQuotation m] (e : Syntax) (mkCont : Syntax → m Code) : m Code := withFreshMacroScope do
 y ← `(y);
 let yName := y.getId;
-auxDo ← `(do let y ← $e:term);
-let doElem := (getDoSeqElems (getDoSeq auxDo)).head!;
+doElem ← `(doElem| let y ← $e:term);
 -- Add elaboration hint for producing sane error message
 y ← `(ensureExpectedType! "type mismatch, result value" $y);
 k ← mkCont y;
@@ -677,14 +679,99 @@ if doElem.getKind == `Lean.Parser.Term.doExpr then
 else
   none
 
--- Code block to syntax term
+/-
+The procedure `ToTerm.run` converts a `CodeBlock` into a `Syntax` term.
+We use this method to convert
+1- The `CodeBlock` for a root `do ...` term into a `Syntax` term. This kind of
+   `CodeBlock` never contains `break` nor `continue`. Moreover, the collection
+   of updated variables is not packed into the result.
+   Thus, we have two kinds of exit points
+     - `Code.action e` which is converted into `e`
+     - `Code.return _ e` which is converted into `pure e`
+
+   We use `Kind.regular` for this case.
+
+2- The `CodeBlock` for `b` at `for x in xs do b`. In this case, we need to generate
+   a `Syntax` term representing a function for the `xs.forIn` combinator.
+
+   a) If `b` contain a `Code.return _ a` exit point. The generated `Syntax` term
+      has type `m (ForInStep (Option α × σ))`, where `a : α`, and the `σ` is the type
+      of the tuple of variables reassigned by `b`.
+      We use `Kind.forInWithReturn` for this case
+
+   b) If `b` does not contain a `Code.return _ a` exit point. Then, the generated
+      `Syntax` term has type `m (ForInStep σ)`.
+      We use `Kind.forIn` for this case.
+
+3- The `CodeBlock` `c` for a `do` sequence nested in a monadic combinator (e.g., `MonadExcept.catch`).
+
+   The generated `Syntax` term for `c` must inform whether `c` "exited" using `Code.action`, `Code.return`,
+   `Code.break` or `Code.continue`. We use the auxiliary types `DoResult`s for storing this information.
+   For example, the auxiliary type `DoResultPBC α σ` is used for a code block that exits with `Code.action`,
+   **and** `Code.break`/`Code.continue`, `α` is the type of values produced by the exit `action`, and
+   `σ` is the type of the tuple of reassigned variables.
+   The type `DoResult α β σ` is usedf for code blocks that exit with
+   `Code.action`, `Code.return`, **and** `Code.break`/`Code.continue`, `β` is the type of the returned values.
+   We don't use `DoResult α β σ` for all cases because:
+
+      a) The elaborator would not be able to infer all type parameters without extra annotations. For example,
+         if the code block does not contain `Code.return _ _`, the elaborator will not be able to infer `β`.
+
+      b) We need to pattern match on the result produced by the combinator (e.g., `MonadExcept.catch`),
+         but we don't want to consider "unreachable" cases.
+
+   We do not distinguish between cases that contain `break`, but not `continue`, and vice versa.
+
+   When listing all cases, we use `a` to indicate the code block contains `Code.action _`, `r` for `Code.return _ _`,
+   and `b/c` for a code block that contains `Code.break _` or `Code.continue _`.
+
+   - `a`: `Kind.regular`, type `m (α × σ)`
+
+   - `r`: `Kind.regular`, type `m (α × σ)`
+           Note that the code that pattern matches on the result will behave differently in this case.
+           It produces `return a` for this case, and `pure a` for the previous one.
+
+   - `b/c`: `Kind.nestedBC`, type `m (DoResultBC σ)`
+
+   - `a` and `r`:   `Kind.nestedPR`, type `m (DoResultPR α β σ)`
+
+   - `a` and `bc`:  `Kind.nestedSBC`, type `m (DoResultSBC α σ)`
+
+   - `r` and `bc`:  `Kind.nestedSBC`, type `m (DoResultSBC α σ)`
+         Again the code that pattern matches on the result will behave differently in this case and
+         the previous one. It produces `return a` for the constructor `DoResultSPR.pureReturn a u` for
+         this case, and `pure a` for the previous case.
+
+   - `a`, `r`, `b/c`: `Kind.nestedPRBC`, type type `m (DoResultPRBC α β σ)`
+
+Here is the recipe for adding new combinators with nested `do`s.
+Example: suppose we want to support `repeat doSeq`. Assuming we have `repeat : m α → m α`
+1- Convert `doSeq` into `codeBlock : CodeBlock`
+2- Create term `term` using `mkNestedTerm code m uvars a r bc` where
+   `code` is `codeBlock.code`, `uvars` is an array containing `codeBlock.uvars`,
+   `m` is a `Syntax` representing the Monad, and
+   `a` is true if `code` contains `Code.action _`,
+   `r` is true if `code` contains `Code.return _ _`,
+   `bc` is true if `code` contains `Code.break _` or `Code.continue _`.
+
+   Remark: for combinators such as `repeat` that take a single `doSeq`, all
+   arguments, but `m`, are extracted from `codeBlock`.
+3- Create the term `repeat $term`
+4- and then, convert it into a `doSeq` using `matchNestedTermResult ref (repeat $term) uvsar a r bc`
+
+-/
 namespace ToTerm
 
 inductive Kind
 | regular
-| forInNestedTerm
 | forIn
 | forInWithReturn
+| nestedBC
+| nestedPR
+| nestedSBC
+| nestedPRBC
+
+instance Kind.inhabited : Inhabited Kind := ⟨Kind.regular⟩
 
 def Kind.isRegular : Kind → Bool
 | Kind.regular => true
@@ -707,9 +794,12 @@ ctx ← read;
 u ← mkUVarTuple ref;
 match ctx.kind with
 | Kind.regular         => if ctx.uvars.isEmpty then `(HasPure.pure $val) else `(HasPure.pure ($val, $u))
-| Kind.forInNestedTerm => `(HasPure.pure (DoResult.«return» $val $u))
 | Kind.forIn           => `(HasPure.pure (ForInStep.done $u))
 | Kind.forInWithReturn => `(HasPure.pure (ForInStep.done (some $val, $u)))
+| Kind.nestedBC        => unreachable!
+| Kind.nestedPR        => `(HasPure.pure (DoResultPR.«return» $val $u))
+| Kind.nestedSBC       => `(HasPure.pure (DoResultSBC.«pureReturn» $val $u))
+| Kind.nestedPRBC      => `(HasPure.pure (DoResultPRBC.«return» $val $u))
 
 def returnToTerm (ref : Syntax) (val : Syntax) : M Syntax := do
 r ← returnToTermCore ref val;
@@ -720,9 +810,12 @@ ctx ← read;
 u ← mkUVarTuple ref;
 match ctx.kind with
 | Kind.regular         => unreachable!
-| Kind.forInNestedTerm => `(HasPure.pure (DoResult.«continue» $u))
 | Kind.forIn           => `(HasPure.pure (ForInStep.yield $u))
 | Kind.forInWithReturn => `(HasPure.pure (ForInStep.yield (none, $u)))
+| Kind.nestedBC        => `(HasPure.pure (DoResultBC.«continue» $u))
+| Kind.nestedPR        => unreachable!
+| Kind.nestedSBC       => `(HasPure.pure (DoResultSBC.«continue» $u))
+| Kind.nestedPRBC      => `(HasPure.pure (DoResultPRBC.«continue» $u))
 
 def continueToTerm (ref : Syntax) : M Syntax := do
 r ← continueToTermCore ref;
@@ -733,9 +826,12 @@ ctx ← read;
 u ← mkUVarTuple ref;
 match ctx.kind with
 | Kind.regular         => unreachable!
-| Kind.forInNestedTerm => `(HasPure.pure (DoResult.«break» $u))
-| Kind.forInWithReturn => `(HasPure.pure (ForInStep.done (none, $u)))
 | Kind.forIn           => `(HasPure.pure (ForInStep.done $u))
+| Kind.forInWithReturn => `(HasPure.pure (ForInStep.done (none, $u)))
+| Kind.nestedBC        => `(HasPure.pure (DoResultBC.«break» $u))
+| Kind.nestedPR        => unreachable!
+| Kind.nestedSBC       => `(HasPure.pure (DoResultSBC.«break» $u))
+| Kind.nestedPRBC      => `(HasPure.pure (DoResultPRBC.«break» $u))
 
 def breakToTerm (ref : Syntax) : M Syntax := do
 r ← breakToTermCore ref;
@@ -746,10 +842,13 @@ let ref := action;
 ctx ← read;
 u ← mkUVarTuple ref;
 match ctx.kind with
-| Kind.forInNestedTerm => `(HasBind.bind $action fun y => (HasPure.pure (DoResult.«pure» y $u)))
+| Kind.regular         => if ctx.uvars.isEmpty then pure action else `(HasBind.bind $action fun y => HasPure.pure (y, $u))
 | Kind.forIn           => `(HasBind.bind $action fun _ => HasPure.pure (ForInStep.yield $u))
 | Kind.forInWithReturn => `(HasBind.bind $action fun _ => HasPure.pure (ForInStep.yield (none, $u)))
-| Kind.regular         => if ctx.uvars.isEmpty then pure action else `(HasBind.bind $action fun y => HasPure.pure (y, $u))
+| Kind.nestedBC        => unreachable!
+| Kind.nestedPR        => `(HasBind.bind $action fun y => (HasPure.pure (DoResultPR.«pure» y $u)))
+| Kind.nestedSBC       => `(HasBind.bind $action fun y => (HasPure.pure (DoResultSBC.«pureReturn» y $u)))
+| Kind.nestedPRBC      => `(HasBind.bind $action fun y => (HasPure.pure (DoResultPRBC.«pure» y $u)))
 
 def actionTerminalToTerm (action : Syntax) : M Syntax := do
 let ref := action;
@@ -904,6 +1003,60 @@ def run (code : Code) (m : Syntax) (uvars : Array Name := #[]) (kind := Kind.reg
 term ← toTerm code { m := m, kind := kind, uvars := uvars };
 pure term
 
+/- Given
+   - `a` is true if the code block has a `Code.action _` exit point
+   - `r` is true if the code block has a `Code.return _ _` exit point
+   - `bc` is true if the code block has a `Code.break _` or `Code.continue _` exit point
+
+   generate Kind. See comment at the beginning of the `ToTerm` namespace. -/
+def mkNestedKind (a r bc : Bool) : Kind :=
+match a, r, bc with
+| true,  false, false => Kind.regular
+| false, true,  false => Kind.regular
+| false, false, true  => Kind.nestedBC
+| true,  true,  false => Kind.nestedPR
+| true,  false, true  => Kind.nestedSBC
+| false, true,  true  => Kind.nestedSBC
+| true,  true,  true  => Kind.nestedPRBC
+| false, false, false => unreachable!
+
+def mkNestedTerm (code : Code) (m : Syntax) (uvars : Array Name) (a r bc : Bool) : MacroM Syntax := do
+ToTerm.run code m uvars (mkNestedKind a r bc)
+
+/- Given a term `term` produced by `ToTerm.run`, pattern match on its result.
+   See comment at the beginning of the `ToTerm` namespace.
+
+   - `a` is true if the code block has a `Code.action _` exit point
+   - `r` is true if the code block has a `Code.return _ _` exit point
+   - `bc` is true if the code block has a `Code.break _` or `Code.continue _` exit point
+
+   The result is a sequence of `doElem` -/
+def matchNestedTermResult (ref : Syntax) (term : Syntax) (uvars : Array Name) (a r bc : Bool) : MacroM (List Syntax) := do
+let toDoElems (auxDo : Syntax) : List Syntax := getDoSeqElems (getDoSeq auxDo);
+u ← mkTuple ref (uvars.map (mkIdentFrom ref));
+match a, r, bc with
+| true, false, false =>
+  if uvars.isEmpty then
+    toDoElems <$> `(do $term:term)
+  else
+    toDoElems <$> `(do let r ← $term:term; $u:term := r.2; pure r.1)
+| false, true, false =>
+  if uvars.isEmpty then
+    toDoElems <$> `(do let r ← $term:term; return r)
+  else
+    toDoElems <$> `(do let r ← $term:term; $u:term := r.2; return r.1)
+| false, false, true => toDoElems <$>
+  `(do let r ← $term:term; match r with | DoResultBC.«break» u => $u:term := u; break | DoResultBC.«continue» u => $u:term := u; continue)
+| true, true, false => toDoElems <$>
+  `(do let r ← $term:term; match r with | DoResultPR.«pure» a u => $u:term := u; pure a | DoResultPR.«return» b u => $u:term := u; return b)
+| true, false, true => toDoElems <$>
+  `(do let r ← $term:term; match r with | DoResultSBC.«pureReturn» a u => $u:term := u; pure a | DoResultSBC.«break» u => $u:term := u; break | DoResultSBC.«continue» u => $u:term := u; continue)
+| false, true, true => toDoElems <$>
+  `(do let r ← $term:term; match r with | DoResultSBC.«pureReturn» a u => $u:term := u; return a | DoResultSBC.«break» u => $u:term := u; break | DoResultSBC.«continue» u => $u:term := u; continue)
+| true, true, true => toDoElems <$>
+  `(do let r ← $term:term; match r with | DoResultPRBC.«pure» a u => $u:term := u; pure a | DoResultPRBC.«return» a u => $u:term := u; return a | DoResultPRBC.«break» u => $u:term := u; break | DoResultPRBC.«continue» u => $u:term := u; continue)
+| false, false, false => unreachable!
+
 end ToTerm
 
 namespace ToCodeBlock
@@ -960,9 +1113,8 @@ private partial def expandLiftMethodAux : Syntax → StateT (List Syntax) MacroM
   else if k == `Lean.Parser.Term.liftMethod then withFreshMacroScope $ do
     let term := args.get! 1;
     term ← expandLiftMethodAux term;
-    auxDo ← `(do let a ← $term:term);
-    let auxDoElems := getDoSeqElems (getDoSeq auxDo);
-    modify fun s => s ++ auxDoElems;
+    auxDoElem ← `(doElem| let a ← $term:term);
+    modify fun s => s ++ [auxDoElem];
     `(a)
   else do
     args ← args.mapM expandLiftMethodAux;
@@ -1138,6 +1290,89 @@ alts : Array (Alt CodeBlock) ←  matchAlts.mapM fun matchAlt => do {
 matchCode ← liftM $ mkMatch ref discrs optType alts;
 concatWith doSeqToCode matchCode doElems
 
+structure Catch :=
+(x         : Syntax)
+(optType   : Syntax)
+(codeBlock : CodeBlock)
+
+def getTryCatchUpdatedVars (tryCode : CodeBlock) (catches : Array Catch) (finallyCode? : Option CodeBlock) : NameSet :=
+let ws := tryCode.uvars;
+let ws := catches.foldl (fun ws alt => union alt.codeBlock.uvars ws) ws;
+let ws := match finallyCode? with
+  | none   => ws
+  | some c => union c.uvars ws;
+ws
+
+def tryCatchPred (tryCode : CodeBlock) (catches : Array Catch) (finallyCode? : Option CodeBlock) (p : Code → Bool) : Bool :=
+p tryCode.code ||
+catches.any (fun catch => p catch.codeBlock.code) ||
+match finallyCode? with
+| none => false
+| some finallyCode => p finallyCode.code
+
+/--
+  Generate `CodeBlock` for `doTry; doElems`
+  ```
+  def doTry := parser! "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
+  def doCatch      := parser! "catch " >> binderIdent >> optional (":" >> termParser) >> darrow >> doSeq
+  def doCatchMatch := parser! "catch " >> doMatchAlts
+  def doFinally    := parser! "finally " >> doSeq
+  ``` -/
+def doTryToCode (doSeqToCode : List Syntax → M CodeBlock) (doTry : Syntax) (doElems: List Syntax) : M CodeBlock := do
+let ref := doTry;
+tryCode ← doSeqToCode (getDoSeqElems (doTry.getArg 1));
+let optFinally := doTry.getArg 3;
+catches ← (doTry.getArg 2).getArgs.mapM fun catchStx => do {
+  if catchStx.getKind == `Lean.Parser.Term.doCatch then do
+    let x       := catchStx.getArg 1;
+    let optType := catchStx.getArg 2;
+    c ← doSeqToCode (getDoSeqElems (catchStx.getArg 4));
+    pure { x := x, optType := optType, codeBlock := c : Catch }
+  else if catchStx.getKind == `Lean.Parser.Term.doCatchMatch then do
+    let matchAlts := catchStx.getArg 1;
+    x ← `(ex);
+    auxDo ← `(do match ex with $matchAlts);
+    c ← doSeqToCode (getDoSeqElems (getDoSeq auxDo));
+    pure { x := x, codeBlock := c, optType := mkNullNode : Catch }
+  else
+    throwError "unexpected kind of 'catch'"
+};
+finallyCode? ← if optFinally.isNone then pure none else some <$> doSeqToCode (getDoSeqElems ((optFinally.getArg 0).getArg 1));
+when (catches.isEmpty && finallyCode?.isNone) $
+  throwError "invalid 'try', it must have a 'catch' or 'finally'";
+ctx ← read;
+let ws    := getTryCatchUpdatedVars tryCode catches finallyCode?;
+let uvars := nameSetToArray ws;
+let a     := tryCatchPred tryCode catches finallyCode? hasTerminalAction;
+let r     := tryCatchPred tryCode catches finallyCode? hasReturn;
+let bc    := tryCatchPred tryCode catches finallyCode? hasBreakContinue;
+let toTerm (codeBlock : CodeBlock) : M Syntax := do {
+  codeBlock ← liftM $ extendUpdatedVars codeBlock ws;
+  liftMacroM $ ToTerm.mkNestedTerm codeBlock.code ctx.m uvars a r bc
+};
+term ← toTerm tryCode;
+term ← catches.foldlM
+  (fun term catch => do
+    catchTerm ← toTerm catch.codeBlock;
+    if catch.optType.isNone then
+      `(MonadExcept.catch $term (fun $(catch.x):ident => $catchTerm))
+    else
+      let type := catch.optType.getArg 1;
+      `(catchThe $type $term (fun $(catch.x):ident => $catchTerm)))
+  term;
+term ← match finallyCode? with
+  | none             => pure term
+  | some finallyCode => withRef optFinally do {
+    unless finallyCode.uvars.isEmpty $
+      throwError $ "'finally' currently does not support reassignments";
+    when (hasBreakContinueReturn finallyCode.code) $
+      throwError $ "'finally' currently does 'return', 'break', nor 'continue'";
+    finallyTerm ← liftMacroM $ ToTerm.run finallyCode.code ctx.m {} ToTerm.Kind.regular;
+    `(«finally» $term $finallyTerm)
+  };
+doElemsNew ← liftMacroM $ ToTerm.matchNestedTermResult ref term uvars a r bc;
+doSeqToCode (doElemsNew ++ doElems)
+
 /- Generate `CodeBlock` for `doReturn` which is of the form
    ```
    "return " >> optional termParser
@@ -1187,7 +1422,7 @@ partial def doSeqToCode : List Syntax → M CodeBlock
     else if k == `Lean.Parser.Term.doMatch then do
       doMatchToCode doSeqToCode doElem doElems
     else if k == `Lean.Parser.Term.doTry then
-      throwError "WIP"
+      doTryToCode doSeqToCode doElem doElems
     else if k == `Lean.Parser.Term.doBreak then do
       ensureInsideFor;
       ensureEOS doElems;

stage0/src/Lean/Elab/Quotation.lean

@@ -136,6 +136,7 @@ stx ← quoteSyntax (elimAntiquotChoices quoted);
 @[builtinTermElab Parser.Tactic.quot] def elabTacticQuot : TermElab := adaptExpander stxQuot.expand
 @[builtinTermElab Parser.Tactic.quotSeq] def elabTacticQuotSeq : TermElab := adaptExpander stxQuot.expand
 @[builtinTermElab Parser.Term.stx.quot] def elabStxQuot : TermElab := adaptExpander stxQuot.expand
+@[builtinTermElab Parser.Term.doElem.quot] def elabDoElemQuot : TermElab := adaptExpander stxQuot.expand
 
 /- match_syntax -/
 

stage0/src/Lean/Parser/Do.lean

@@ -76,7 +76,7 @@ def doMatchAlt : Parser  := parser! sepBy1 termParser ", " >> darrow >> doSeq
 def doMatchAlts : Parser := parser! withPosition $ (optional "| ") >> sepBy1 doMatchAlt (checkColGe "alternatives must be indented" >> "| ")
 @[builtinDoElemParser] def doMatch := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> doMatchAlts
 
-def doCatch      := parser! «try» ("catch " >> binderIdent) >> optional binderType >> darrow >> doSeq
+def doCatch      := parser! «try» ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq
 def doCatchMatch := parser! "catch " >> doMatchAlts
 def doFinally    := parser! "finally " >> doSeq
 @[builtinDoElemParser] def doTry    := parser! "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally

stage0/src/Lean/Parser/StrInterpolation.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Parser.Basic
+new_frontend
+namespace Lean.Parser
+
+def isQuotableCharForStrInterpolant (c : Char) : Bool :=
+c == '{' || isQuotableCharDefault c
+
+partial def interpolatedStrFn (p : ParserFn) : ParserFn :=
+fun c s =>
+let input     := c.input
+let stackSize := s.stackSize
+let rec parse (startPos : Nat) (c : ParserContext) (s : ParserState) : ParserState :=
+  let i     := s.pos
+  if input.atEnd i then
+    s.mkEOIError
+  else
+    let curr := input.get i
+    let s    := s.setPos (input.next i)
+    if curr == '\"' then
+      let s := mkNodeToken interpolatedStrLitKind startPos c s
+      s.mkNode interpolatedStrKind stackSize
+    else if curr == '\\' then
+      andthenFn (quotedCharCoreFn isQuotableCharForStrInterpolant) (parse startPos) c s
+    else if curr == '{' then
+      let s := mkNodeToken interpolatedStrLitKind startPos c s
+      let s := p c s
+      if s.hasError then s
+      else
+        let pos := s.pos
+        andthenFn (satisfyFn (· == '}') "expected '}'") (parse pos) c s
+    else
+      parse startPos c s
+let startPos := s.pos
+if input.atEnd startPos then
+  s.mkEOIError
+else
+  let s := s.next input startPos
+  parse startPos c s
+
+@[inline] def interpolatedStrNoAntiquot (p : Parser) : Parser :=
+{ fn   := interpolatedStrFn p.fn,
+  info := mkAtomicInfo "interpolatedStr" }
+
+def interpolatedStr (p : Parser) : Parser :=
+withAntiquot (mkAntiquot "interpolatedStr" interpolatedStrKind) $ interpolatedStrNoAntiquot p
+
+end Lean.Parser

stage0/src/Lean/PrettyPrinter/Formatter.lean

@@ -15,6 +15,7 @@ already know the text following it and can decide whether or not whitespace betw
 
 import Lean.CoreM
 import Lean.Parser.Extension
+import Lean.Parser.StrInterpolation
 import Lean.KeyedDeclsAttribute
 import Lean.ParserCompiler.Attribute
 import Lean.PrettyPrinter.Backtrack
@@ -418,6 +419,10 @@ concatArgs do
   visitAtom Name.anonymous;
   push "`"; goLeft
 
+@[combinatorFormatter Lean.Parser.interpolatedStr]
+def interpolatedStr.formatter (p : Formatter) : Formatter :=
+throwError "NIY"
+
 @[combinatorFormatter unquotedSymbol] def unquotedSymbol.formatter := visitAtom Name.anonymous
 
 @[combinatorFormatter ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Formatter) : Formatter :=

stage0/src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -74,6 +74,7 @@ node).
 import Lean.CoreM
 import Lean.KeyedDeclsAttribute
 import Lean.Parser.Extension
+import Lean.Parser.StrInterpolation
 import Lean.ParserCompiler.Attribute
 import Lean.PrettyPrinter.Backtrack
 
@@ -458,6 +459,10 @@ p
 @[combinatorParenthesizer Lean.Parser.quotedSymbol] def quotedSymbol.parenthesizer := visitToken
 @[combinatorParenthesizer Lean.Parser.unquotedSymbol] def unquotedSymbol.parenthesizer := visitToken
 
+@[combinatorParenthesizer Lean.Parser.interpolatedStr]
+def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer :=
+throwError "NIY"
+
 @[combinatorParenthesizer ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Parenthesizer) : Parenthesizer :=
 if c then t else e
 

stage0/stdlib/Init/Data/Array.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Data.Array
-// Imports: Init.Data.Array.Basic Init.Data.Array.QSort Init.Data.Array.BinSearch
+// Imports: Init.Data.Array.Basic Init.Data.Array.QSort Init.Data.Array.BinSearch Init.Data.Array.ForIn
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -16,6 +16,7 @@ extern "C" {
 lean_object* initialize_Init_Data_Array_Basic(lean_object*);
 lean_object* initialize_Init_Data_Array_QSort(lean_object*);
 lean_object* initialize_Init_Data_Array_BinSearch(lean_object*);
+lean_object* initialize_Init_Data_Array_ForIn(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Data_Array(lean_object* w) {
 lean_object * res;
@@ -30,6 +31,9 @@ lean_dec_ref(res);
 res = initialize_Init_Data_Array_BinSearch(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Data_Array_ForIn(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Init/Data/Array/ForIn.c

@@ -0,0 +1,421 @@
+// Lean compiler output
+// Module: Init.Data.Array.ForIn
+// Imports: Init.Data.Array.Basic
+#include <lean/lean.h>
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+size_t l_USize_add(size_t, size_t);
+lean_object* lean_array_uget(lean_object*, size_t);
+lean_object* l_Array_forIn_loop_match__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_array_get_size(lean_object*);
+uint8_t l_USize_decLt(size_t, size_t);
+lean_object* l_Array_forIn(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forIn_loop(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forIn_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forIn_loop_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
+lean_object* lean_array_fget(lean_object*, lean_object*);
+uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
+lean_object* l_Array_forIn___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe(lean_object*, lean_object*, lean_object*);
+lean_object* lean_nat_sub(lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop_match__1(lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forIn_loop_match__2(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forIn_loop_match__2___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forIn_loop___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop___rarg___lambda__1(lean_object*, size_t, lean_object*, lean_object*, size_t, lean_object*);
+lean_object* l_Array_forInUnsafe_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forIn_loop___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+size_t lean_usize_of_nat(lean_object*);
+lean_object* l_Array_forIn_loop___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forIn_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forIn_loop_match__1(lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+lean_dec(x_3);
+x_4 = lean_ctor_get(x_1, 0);
+lean_inc(x_4);
+lean_dec(x_1);
+x_5 = lean_apply_1(x_2, x_4);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_2);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_1(x_3, x_6);
+return x_7;
+}
+}
+}
+lean_object* l_Array_forInUnsafe_loop_match__1(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop_match__1___rarg), 3, 0);
+return x_3;
+}
+}
+lean_object* l_Array_forInUnsafe_loop___rarg___lambda__1(lean_object* x_1, size_t x_2, lean_object* x_3, lean_object* x_4, size_t x_5, lean_object* x_6) {
+_start:
+{
+if (lean_obj_tag(x_6) == 0)
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
+lean_dec(x_4);
+lean_dec(x_3);
+x_7 = lean_ctor_get(x_6, 0);
+lean_inc(x_7);
+lean_dec(x_6);
+x_8 = lean_ctor_get(x_1, 0);
+lean_inc(x_8);
+lean_dec(x_1);
+x_9 = lean_ctor_get(x_8, 1);
+lean_inc(x_9);
+lean_dec(x_8);
+x_10 = lean_apply_2(x_9, lean_box(0), x_7);
+return x_10;
+}
+else
+{
+lean_object* x_11; size_t x_12; size_t x_13; lean_object* x_14; 
+x_11 = lean_ctor_get(x_6, 0);
+lean_inc(x_11);
+lean_dec(x_6);
+x_12 = 1;
+x_13 = x_2 + x_12;
+x_14 = l_Array_forInUnsafe_loop___rarg(x_1, x_3, x_4, x_5, x_13, x_11);
+return x_14;
+}
+}
+}
+lean_object* l_Array_forInUnsafe_loop___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, size_t x_4, size_t x_5, lean_object* x_6) {
+_start:
+{
+uint8_t x_7; 
+x_7 = x_5 < x_4;
+if (x_7 == 0)
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; 
+lean_dec(x_3);
+lean_dec(x_2);
+x_8 = lean_ctor_get(x_1, 0);
+lean_inc(x_8);
+lean_dec(x_1);
+x_9 = lean_ctor_get(x_8, 1);
+lean_inc(x_9);
+lean_dec(x_8);
+x_10 = lean_apply_2(x_9, lean_box(0), x_6);
+return x_10;
+}
+else
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_11 = lean_array_uget(x_2, x_5);
+x_12 = lean_ctor_get(x_1, 1);
+lean_inc(x_12);
+lean_inc(x_3);
+x_13 = lean_apply_2(x_3, x_11, x_6);
+x_14 = lean_box_usize(x_5);
+x_15 = lean_box_usize(x_4);
+x_16 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___rarg___lambda__1___boxed), 6, 5);
+lean_closure_set(x_16, 0, x_1);
+lean_closure_set(x_16, 1, x_14);
+lean_closure_set(x_16, 2, x_2);
+lean_closure_set(x_16, 3, x_3);
+lean_closure_set(x_16, 4, x_15);
+x_17 = lean_apply_4(x_12, lean_box(0), lean_box(0), x_13, x_16);
+return x_17;
+}
+}
+}
+lean_object* l_Array_forInUnsafe_loop(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___rarg___boxed), 6, 0);
+return x_4;
+}
+}
+lean_object* l_Array_forInUnsafe_loop___rarg___lambda__1___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:
+{
+size_t x_7; size_t x_8; lean_object* x_9; 
+x_7 = lean_unbox_usize(x_2);
+lean_dec(x_2);
+x_8 = lean_unbox_usize(x_5);
+lean_dec(x_5);
+x_9 = l_Array_forInUnsafe_loop___rarg___lambda__1(x_1, x_7, x_3, x_4, x_8, x_6);
+return x_9;
+}
+}
+lean_object* l_Array_forInUnsafe_loop___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:
+{
+size_t x_7; size_t x_8; lean_object* x_9; 
+x_7 = lean_unbox_usize(x_4);
+lean_dec(x_4);
+x_8 = lean_unbox_usize(x_5);
+lean_dec(x_5);
+x_9 = l_Array_forInUnsafe_loop___rarg(x_1, x_2, x_3, x_7, x_8, x_6);
+return x_9;
+}
+}
+lean_object* l_Array_forInUnsafe___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; size_t x_6; size_t x_7; lean_object* x_8; 
+x_5 = lean_array_get_size(x_2);
+x_6 = lean_usize_of_nat(x_5);
+lean_dec(x_5);
+x_7 = 0;
+x_8 = l_Array_forInUnsafe_loop___rarg(x_1, x_2, x_4, x_6, x_7, x_3);
+return x_8;
+}
+}
+lean_object* l_Array_forInUnsafe(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_Array_forInUnsafe___rarg), 4, 0);
+return x_4;
+}
+}
+lean_object* l_Array_forIn_loop_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+lean_dec(x_3);
+x_4 = lean_ctor_get(x_1, 0);
+lean_inc(x_4);
+lean_dec(x_1);
+x_5 = lean_apply_1(x_2, x_4);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_2);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_1(x_3, x_6);
+return x_7;
+}
+}
+}
+lean_object* l_Array_forIn_loop_match__1(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_closure((void*)(l_Array_forIn_loop_match__1___rarg), 3, 0);
+return x_3;
+}
+}
+lean_object* l_Array_forIn_loop_match__2___rarg(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_unsigned_to_nat(0u);
+x_6 = lean_nat_dec_eq(x_1, x_5);
+if (x_6 == 0)
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+lean_dec(x_3);
+x_7 = lean_unsigned_to_nat(1u);
+x_8 = lean_nat_sub(x_1, x_7);
+x_9 = lean_apply_2(x_4, x_8, lean_box(0));
+return x_9;
+}
+else
+{
+lean_object* x_10; 
+lean_dec(x_4);
+x_10 = lean_apply_1(x_3, lean_box(0));
+return x_10;
+}
+}
+}
+lean_object* l_Array_forIn_loop_match__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_Array_forIn_loop_match__2___rarg___boxed), 4, 0);
+return x_4;
+}
+}
+lean_object* l_Array_forIn_loop_match__2___rarg___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_Array_forIn_loop_match__2___rarg(x_1, x_2, x_3, x_4);
+lean_dec(x_1);
+return x_5;
+}
+}
+lean_object* l_Array_forIn_loop_match__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Array_forIn_loop_match__2(x_1, x_2, x_3);
+lean_dec(x_2);
+return x_4;
+}
+}
+lean_object* l_Array_forIn_loop___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+if (lean_obj_tag(x_5) == 0)
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+lean_dec(x_3);
+lean_dec(x_2);
+x_6 = lean_ctor_get(x_5, 0);
+lean_inc(x_6);
+lean_dec(x_5);
+x_7 = lean_ctor_get(x_1, 0);
+lean_inc(x_7);
+lean_dec(x_1);
+x_8 = lean_ctor_get(x_7, 1);
+lean_inc(x_8);
+lean_dec(x_7);
+x_9 = lean_apply_2(x_8, lean_box(0), x_6);
+return x_9;
+}
+else
+{
+lean_object* x_10; lean_object* x_11; 
+x_10 = lean_ctor_get(x_5, 0);
+lean_inc(x_10);
+lean_dec(x_5);
+x_11 = l_Array_forIn_loop___rarg(x_1, x_2, x_3, x_4, lean_box(0), x_10);
+return x_11;
+}
+}
+}
+lean_object* l_Array_forIn_loop___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; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_9 = lean_unsigned_to_nat(1u);
+x_10 = lean_nat_sub(x_4, x_9);
+x_11 = lean_ctor_get(x_1, 1);
+lean_inc(x_11);
+x_12 = lean_array_get_size(x_2);
+x_13 = lean_nat_sub(x_12, x_9);
+lean_dec(x_12);
+x_14 = lean_nat_sub(x_13, x_10);
+lean_dec(x_13);
+x_15 = lean_array_fget(x_2, x_14);
+lean_dec(x_14);
+lean_inc(x_3);
+x_16 = lean_apply_2(x_3, x_15, x_6);
+x_17 = lean_alloc_closure((void*)(l_Array_forIn_loop___rarg___lambda__1___boxed), 5, 4);
+lean_closure_set(x_17, 0, x_1);
+lean_closure_set(x_17, 1, x_2);
+lean_closure_set(x_17, 2, x_3);
+lean_closure_set(x_17, 3, x_10);
+x_18 = lean_apply_4(x_11, lean_box(0), lean_box(0), x_16, x_17);
+return x_18;
+}
+else
+{
+lean_object* x_19; lean_object* x_20; lean_object* x_21; 
+lean_dec(x_3);
+lean_dec(x_2);
+x_19 = lean_ctor_get(x_1, 0);
+lean_inc(x_19);
+lean_dec(x_1);
+x_20 = lean_ctor_get(x_19, 1);
+lean_inc(x_20);
+lean_dec(x_19);
+x_21 = lean_apply_2(x_20, lean_box(0), x_6);
+return x_21;
+}
+}
+}
+lean_object* l_Array_forIn_loop(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_Array_forIn_loop___rarg___boxed), 6, 0);
+return x_4;
+}
+}
+lean_object* l_Array_forIn_loop___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+lean_object* x_6; 
+x_6 = l_Array_forIn_loop___rarg___lambda__1(x_1, x_2, x_3, x_4, x_5);
+lean_dec(x_4);
+return x_6;
+}
+}
+lean_object* l_Array_forIn_loop___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_Array_forIn_loop___rarg(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_4);
+return x_7;
+}
+}
+lean_object* l_Array_forIn___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; 
+x_5 = lean_array_get_size(x_2);
+x_6 = l_Array_forIn_loop___rarg(x_1, x_2, x_4, x_5, lean_box(0), x_3);
+lean_dec(x_5);
+return x_6;
+}
+}
+lean_object* l_Array_forIn(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_Array_forIn___rarg), 4, 0);
+return x_4;
+}
+}
+lean_object* initialize_Init_Data_Array_Basic(lean_object*);
+static bool _G_initialized = false;
+lean_object* initialize_Init_Data_Array_ForIn(lean_object* w) {
+lean_object * res;
+if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
+_G_initialized = true;
+res = initialize_Init_Data_Array_Basic(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+return lean_io_result_mk_ok(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif

stage0/stdlib/Init/Data/Fin/Basic.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Data.Fin.Basic
-// Imports: Init.Data.Nat.Div Init.Data.Nat.Bitwise
+// Imports: Init.Data.Nat.Div Init.Data.Nat.Bitwise Init.Coe
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -19,6 +19,7 @@ lean_object* l_Fin_decLt___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Fin_ofNat(lean_object*, lean_object*);
 lean_object* l_Fin_elim0___boxed(lean_object*, lean_object*);
 lean_object* l_Fin_land(lean_object*, lean_object*, lean_object*);
+lean_object* l_Fin_coeToNat(lean_object*);
 lean_object* l_Fin_DecidableEq(lean_object*);
 uint8_t l_Fin_decLe___rarg(lean_object*, lean_object*);
 lean_object* l_Fin_HasOne(lean_object*);
@@ -35,6 +36,7 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l_Fin_ofNat_x27(lean_object*, lean_object*, lean_object*);
 lean_object* l_Fin_HasAdd(lean_object*);
 lean_object* lean_nat_sub(lean_object*, lean_object*);
+lean_object* l_Fin_coeToNat___boxed(lean_object*);
 lean_object* l_Fin_add(lean_object*, lean_object*, lean_object*);
 lean_object* l_Fin_ofNat_x27___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Fin_sub(lean_object*, lean_object*, lean_object*);
@@ -59,6 +61,7 @@ lean_object* lean_nat_mul(lean_object*, lean_object*);
 lean_object* l_Fin_elim0(lean_object*, lean_object*);
 lean_object* l_Fin_mod(lean_object*, lean_object*, lean_object*);
 lean_object* l_Fin_mul(lean_object*, lean_object*, lean_object*);
+lean_object* l_Fin_coeToNat___rarg(lean_object*);
 lean_object* l_Fin_decLe___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Fin_HasOne___boxed(lean_object*);
 lean_object* l_Fin_modn(lean_object*, lean_object*, lean_object*);
@@ -70,7 +73,41 @@ lean_object* lean_nat_mod(lean_object*, lean_object*);
 lean_object* l_Fin_DecidableEq___boxed(lean_object*);
 lean_object* l_Fin_HasDiv(lean_object*);
 lean_object* l_Fin_div___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Fin_coeToNat___rarg___boxed(lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
+lean_object* l_Fin_coeToNat___rarg(lean_object* x_1) {
+_start:
+{
+lean_inc(x_1);
+return x_1;
+}
+}
+lean_object* l_Fin_coeToNat(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Fin_coeToNat___rarg___boxed), 1, 0);
+return x_2;
+}
+}
+lean_object* l_Fin_coeToNat___rarg___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Fin_coeToNat___rarg(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
+lean_object* l_Fin_coeToNat___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Fin_coeToNat(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
 lean_object* l_Fin_HasLess(lean_object* x_1) {
 _start:
 {
@@ -524,6 +561,7 @@ return x_2;
 }
 lean_object* initialize_Init_Data_Nat_Div(lean_object*);
 lean_object* initialize_Init_Data_Nat_Bitwise(lean_object*);
+lean_object* initialize_Init_Coe(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Data_Fin_Basic(lean_object* w) {
 lean_object * res;
@@ -535,6 +573,9 @@ lean_dec_ref(res);
 res = initialize_Init_Data_Nat_Bitwise(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Coe(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Init/LeanInit.c

@@ -35,6 +35,7 @@ lean_object* l___private_Init_LeanInit_1__eraseMacroScopesAux___main___closed__1
 lean_object* l_Lean_Macro_monadQuotation___lambda__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_eraseMacroScopes(lean_object*);
 lean_object* l_Lean_Syntax_isNatLitAux(lean_object*, lean_object*);
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar_match__1(lean_object*);
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 lean_object* l_Lean_MacroScopesView_inhabited;
 lean_object* l_Array_iterateMAux___main___at_Lean_mkSepArray___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -53,6 +54,7 @@ extern lean_object* l_Option_HasRepr___rarg___closed__1;
 uint32_t l_Lean_idBeginEscape;
 lean_object* l___private_Init_LeanInit_14__quoteList___main___rarg___closed__7;
 lean_object* l_Lean_Macro_monadQuotationTrans___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_expandInterpolatedStrChunks(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_decodeQuotedChar(lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_5__extractMainModule(lean_object*, lean_object*, lean_object*);
 uint8_t lean_name_eq(lean_object*, lean_object*);
@@ -82,6 +84,7 @@ lean_object* l_Lean_Syntax_isOfKind___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_HasBeq;
 lean_object* l_Lean_fieldIdxKind___closed__1;
 lean_object* l_Lean_Macro_mkMacroEnvSimple;
+lean_object* l_Lean_Syntax_isInterpolatedStrLit_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t l_Char_isDigit(uint32_t);
 lean_object* l_Lean_charLitKind___closed__2;
 lean_object* l_Lean_Substring_HasQuote(lean_object*);
@@ -99,6 +102,7 @@ lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
 uint8_t l_Lean_isIdBeginEscape(uint32_t);
 lean_object* l_Lean_Substring_HasQuote___boxed(lean_object*);
 lean_object* l_Lean_Macro_withFreshMacroScope(lean_object*);
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit_loop(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_15__quoteOption___rarg___closed__3;
 lean_object* l_Lean_Name_HasToString___closed__1;
 lean_object* l_Lean_mkNameSimple(lean_object*);
@@ -112,6 +116,7 @@ lean_object* lean_array_get_size(lean_object*);
 lean_object* l_Lean_Prod_hasQuote___rarg___closed__2;
 lean_object* l_Lean_charLitKind___closed__1;
 lean_object* lean_string_append(lean_object*, lean_object*);
+lean_object* l_Lean_interpolatedStrKind;
 lean_object* l_Lean_Macro_expandMacroNotAvailable_x3f(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_14__quoteList___main___rarg___closed__5;
 lean_object* l___private_Init_LeanInit_17__mapSepElemsMAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -122,6 +127,7 @@ lean_object* l___private_Init_LeanInit_7__decodeBinLitAux___main(lean_object*, l
 lean_object* l_Lean_Syntax_identToStrLit(lean_object*);
 lean_object* l___private_Init_LeanInit_14__quoteList(lean_object*);
 lean_object* l_Lean_Name_hashable___closed__1;
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit___boxed(lean_object*);
 lean_object* l_Array_filterSepElemsM___at_Array_filterSepElems___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Macro_MacroEnv_inhabited;
 lean_object* l___private_Init_LeanInit_16__filterSepElemsMAux___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
@@ -138,6 +144,7 @@ lean_object* l_Lean_nameLitKind;
 lean_object* l_Lean_Macro_monadQuotationTrans(lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_15__quoteOption___rarg___closed__4;
 lean_object* l___private_Init_LeanInit_14__quoteList___main___rarg___closed__3;
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit_loop_match__1(lean_object*);
 lean_object* l_Lean_mkAppStx___closed__8;
 lean_object* l_Lean_maxRecDepthErrorMessage___closed__1;
 lean_object* l_Lean_mkAppStx___closed__7;
@@ -148,6 +155,7 @@ lean_object* l_Array_mapSepElems(lean_object*, lean_object*);
 lean_object* l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1(lean_object*);
 lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*);
 lean_object* l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_interpolatedStrLitKind___closed__2;
 lean_object* l_Lean_Syntax_getKind___closed__2;
 lean_object* l_Lean_Syntax_getKind___closed__1;
 lean_object* l___private_Init_LeanInit_11__decodeDecimalLitAux___boxed(lean_object*, lean_object*, lean_object*);
@@ -174,8 +182,10 @@ lean_object* l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1___rar
 lean_object* l_Lean_Macro_MacroEnvPointed;
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_findAux___main(lean_object*, lean_object*);
+lean_object* l_Lean_interpolatedStrLitKind___closed__1;
 lean_object* l_Lean_numLitKind;
 lean_object* l_Lean_choiceKind___closed__1;
+lean_object* l_Lean_Syntax_expandInterpolatedStrChunks_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Macro_expandMacroNotAvailable_x3f___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_mapSepElemsM(lean_object*);
 lean_object* lean_nat_sub(lean_object*, lean_object*);
@@ -194,6 +204,7 @@ lean_object* l___private_Init_LeanInit_15__quoteOption___rarg___closed__2;
 lean_object* l_Lean_Syntax_isFieldIdx_x3f(lean_object*);
 lean_object* l_Lean_Macro_addMacroScope(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getHeadInfo(lean_object*);
+lean_object* l_Lean_Syntax_expandInterpolatedStrChunks_match__1(lean_object*);
 lean_object* l_Lean_Macro_withIncRecDepth___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_toString(lean_object*);
 lean_object* l_Lean_firstFrontendMacroScope___closed__1;
@@ -207,6 +218,7 @@ lean_object* l___private_Init_LeanInit_1__eraseMacroScopesAux(lean_object*);
 lean_object* l_Lean_strLitKind___closed__1;
 lean_object* l_Lean_Syntax_isNatLitAux___boxed(lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_4__extractImported___main(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_16__filterSepElemsMAux(lean_object*);
 lean_object* l_Lean_NameGenerator_Inhabited___closed__2;
@@ -227,6 +239,7 @@ lean_object* l_Lean_Name_HasToString;
 lean_object* l_Lean_Macro_expandMacro_x3f___rarg(lean_object*);
 lean_object* l_Lean_Macro_expandMacroNotAvailable_x3f___closed__1;
 lean_object* l_Array_umapMAux___main___at_Lean_expandMacros___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_isInterpolatedStrLit_x3f_match__1(lean_object*);
 lean_object* l_Lean_Name_hasQuote;
 lean_object* l_Lean_Syntax_getId(lean_object*);
 lean_object* l_Lean_expandMacros___main(lean_object*, lean_object*, lean_object*);
@@ -252,10 +265,13 @@ lean_object* l_Nat_pred(lean_object*);
 lean_object* l___private_Init_LeanInit_14__quoteList___main___rarg___closed__1;
 lean_object* l___private_Init_LeanInit_15__quoteOption___rarg(lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_17__mapSepElemsMAux___main___at_Array_mapSepElems___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit(lean_object*);
+lean_object* l_Lean_interpolatedStrKind___closed__2;
 lean_object* l___private_Init_LeanInit_13__quoteName___main___closed__3;
 uint8_t l_Array_isEmpty___rarg(lean_object*);
 lean_object* l_Lean_Name_toStringWithSep___boxed(lean_object*, lean_object*);
 lean_object* l_Array_filterSepElemsM(lean_object*);
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit_loop_match__1___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_firstFrontendMacroScope;
 lean_object* l_Lean_ParserDescr_inhabited___closed__1;
 lean_object* l_Lean_mkSepArray(lean_object*, lean_object*);
@@ -266,6 +282,7 @@ lean_object* l_Substring_takeWhileAux___main___at___private_Init_LeanInit_12__de
 lean_object* l_Lean_SourceInfo_inhabited;
 size_t lean_usize_of_nat(lean_object*);
 lean_object* l_Lean_nullKind___closed__1;
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar___boxed__const__1;
 lean_object* l_Lean_Syntax_decodeStrLit___boxed(lean_object*);
 lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_isIdEndEscape(uint32_t);
@@ -292,6 +309,7 @@ lean_object* l_Lean_Macro_monadQuotation___lambda__2___boxed(lean_object*, lean_
 lean_object* l_Lean_isLetterLike___boxed(lean_object*);
 lean_object* l_Lean_Syntax_isIdOrAtom_x3f(lean_object*);
 uint8_t l_Lean_Name_hasMacroScopes___main(lean_object*);
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Array_hasQuote(lean_object*);
 lean_object* l_Lean_Syntax_decodeQuotedChar___boxed__const__2;
 lean_object* l_Lean_identKind;
@@ -305,6 +323,7 @@ lean_object* l___private_Init_LeanInit_16__filterSepElemsMAux___main___rarg(lean
 lean_object* l_Lean_Macro_throwError___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_6__extractMacroScopesAux___main(lean_object*, lean_object*);
 lean_object* l_Lean_mkHole(lean_object*);
+lean_object* l_Lean_Syntax_expandInterpolatedStrChunks___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Syntax_hasArgs(lean_object*);
 lean_object* l___private_Init_LeanInit_4__extractImported(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Macro_withIncRecDepth(lean_object*);
@@ -353,6 +372,7 @@ lean_object* l_Lean_expandMacros(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_decodeNameLit(lean_object*);
 lean_object* l_Lean_mkOptionalNode___closed__1;
 lean_object* l_Lean_Syntax_isNameLit_x3f(lean_object*);
+lean_object* l_Lean_Syntax_isInterpolatedStrLit_x3f(lean_object*);
 lean_object* l_Lean_Macro_expandMacro_x3fImp(lean_object*, lean_object*, lean_object*);
 lean_object* l_String_trim(lean_object*);
 lean_object* l_Lean_Syntax_decodeQuotedChar___boxed(lean_object*, lean_object*);
@@ -360,8 +380,10 @@ lean_object* l_Lean_isIdEndEscape___boxed(lean_object*);
 lean_object* l_Lean_Syntax_getOptionalIdent_x3f___boxed(lean_object*);
 lean_object* l_Array_toList___rarg(lean_object*);
 lean_object* l_Lean_Macro_monadQuotation___closed__1;
+lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_expandInterpolatedStrChunks___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_decodeStrLit(lean_object*);
 uint8_t l_Lean_isIdFirst(uint32_t);
+lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_expandInterpolatedStrChunks___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_13__quoteName___main(lean_object*);
 uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
 size_t lean_usize_mix_hash(size_t, size_t);
@@ -378,6 +400,7 @@ lean_object* l___private_Init_LeanInit_14__quoteList___main___rarg___closed__6;
 lean_object* l_Lean_Syntax_decodeQuotedChar___boxed__const__3;
 lean_object* l_Lean_ParserDescr_inhabited;
 lean_object* l___private_Init_LeanInit_13__quoteName___main___closed__6;
+lean_object* l_Lean_Syntax_isInterpolatedStrLit_x3f___boxed(lean_object*);
 lean_object* l_Lean_Syntax_decodeNameLit___boxed(lean_object*);
 lean_object* lean_string_length(lean_object*);
 lean_object* l_Lean_Macro_withFreshMacroScope___rarg(lean_object*, lean_object*, lean_object*);
@@ -386,6 +409,7 @@ uint8_t l_Lean_isSubScriptAlnum(uint32_t);
 lean_object* l_List_foldl___main___at_Lean_MacroScopesView_review___spec__1(lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_16__filterSepElemsMAux___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Macro_monadQuotation___closed__4;
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar(lean_object*, lean_object*);
 lean_object* l_Lean_Macro_monadQuotation;
 lean_object* l_Lean_Macro_throwUnsupported(lean_object*, lean_object*);
 lean_object* lean_mk_syntax_ident(lean_object*);
@@ -396,6 +420,7 @@ lean_object* l_Lean_mkOptionalNode___closed__2;
 lean_object* l_Lean_Syntax_getOptional_x3f___boxed(lean_object*);
 lean_object* l_Lean_mkCIdentFrom___closed__2;
 lean_object* lean_nat_mod(lean_object*, lean_object*);
+lean_object* l_Lean_interpolatedStrKind___closed__1;
 lean_object* l_Lean_Name_eraseMacroScopes___boxed(lean_object*);
 lean_object* l___private_Init_LeanInit_2__simpMacroScopesAux(lean_object*);
 lean_object* l___private_Init_LeanInit_11__decodeDecimalLitAux(lean_object*, lean_object*, lean_object*);
@@ -448,8 +473,10 @@ size_t lean_string_hash(lean_object*);
 lean_object* l___private_Init_LeanInit_7__decodeBinLitAux___main___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_1__eraseMacroScopesAux___main___boxed(lean_object*);
 lean_object* l_Lean_Option_hasQuote___rarg(lean_object*);
+lean_object* l_Lean_interpolatedStrLitKind;
 lean_object* l_Lean_Name_append___boxed(lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_16__filterSepElemsMAux___main___at_Array_filterSepElems___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit_loop___boxed(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_isIdRest(uint32_t);
 lean_object* l_Lean_NameGenerator_Inhabited___closed__3;
 lean_object* l_Lean_Syntax_isIdent___boxed(lean_object*);
@@ -1929,6 +1956,58 @@ x_1 = l_Lean_fieldIdxKind___closed__2;
 return x_1;
 }
 }
+lean_object* _init_l_Lean_interpolatedStrLitKind___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("interpolatedStrLitKind");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_interpolatedStrLitKind___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_interpolatedStrLitKind___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_interpolatedStrLitKind() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_interpolatedStrLitKind___closed__2;
+return x_1;
+}
+}
+lean_object* _init_l_Lean_interpolatedStrKind___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("interpolatedStrKind");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_interpolatedStrKind___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_interpolatedStrKind___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_interpolatedStrKind() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_interpolatedStrKind___closed__2;
+return x_1;
+}
+}
 lean_object* _init_l_Lean_Syntax_getKind___closed__1() {
 _start:
 {
@@ -8233,6 +8312,627 @@ lean_dec(x_1);
 return x_3;
 }
 }
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+lean_dec(x_2);
+x_4 = lean_box(0);
+x_5 = lean_apply_1(x_3, x_4);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_3);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_1(x_2, x_6);
+return x_7;
+}
+}
+}
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar_match__1___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* _init_l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar___boxed__const__1() {
+_start:
+{
+uint32_t x_1; lean_object* x_2; 
+x_1 = 123;
+x_2 = lean_box_uint32(x_1);
+return x_2;
+}
+}
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Syntax_decodeQuotedChar(x_1, x_2);
+if (lean_obj_tag(x_3) == 0)
+{
+uint32_t x_4; lean_object* x_5; uint32_t x_6; uint8_t x_7; 
+x_4 = lean_string_utf8_get(x_1, x_2);
+x_5 = lean_string_utf8_next(x_1, x_2);
+x_6 = 123;
+x_7 = x_4 == x_6;
+if (x_7 == 0)
+{
+lean_object* x_8; 
+lean_dec(x_5);
+x_8 = lean_box(0);
+return x_8;
+}
+else
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_9 = l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar___boxed__const__1;
+x_10 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_10, 0, x_9);
+lean_ctor_set(x_10, 1, x_5);
+x_11 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_11, 0, x_10);
+return x_11;
+}
+}
+else
+{
+uint8_t x_12; 
+x_12 = !lean_is_exclusive(x_3);
+if (x_12 == 0)
+{
+return x_3;
+}
+else
+{
+lean_object* x_13; lean_object* x_14; 
+x_13 = lean_ctor_get(x_3, 0);
+lean_inc(x_13);
+lean_dec(x_3);
+x_14 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_14, 0, x_13);
+return x_14;
+}
+}
+}
+}
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit_loop_match__1___rarg(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_3 = lean_ctor_get(x_1, 0);
+lean_inc(x_3);
+x_4 = lean_ctor_get(x_1, 1);
+lean_inc(x_4);
+lean_dec(x_1);
+x_5 = lean_apply_2(x_2, x_3, x_4);
+return x_5;
+}
+}
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit_loop_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit_loop_match__1___rarg), 2, 0);
+return x_2;
+}
+}
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit_loop(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+uint32_t x_4; lean_object* x_5; uint8_t x_6; uint32_t x_23; uint8_t x_24; 
+x_4 = lean_string_utf8_get(x_1, x_2);
+x_5 = lean_string_utf8_next(x_1, x_2);
+lean_dec(x_2);
+x_23 = 34;
+x_24 = x_4 == x_23;
+if (x_24 == 0)
+{
+uint32_t x_25; uint8_t x_26; 
+x_25 = 123;
+x_26 = x_4 == x_25;
+if (x_26 == 0)
+{
+uint8_t x_27; 
+x_27 = 0;
+x_6 = x_27;
+goto block_22;
+}
+else
+{
+uint8_t x_28; 
+x_28 = 1;
+x_6 = x_28;
+goto block_22;
+}
+}
+else
+{
+uint8_t x_29; 
+x_29 = 1;
+x_6 = x_29;
+goto block_22;
+}
+block_22:
+{
+if (x_6 == 0)
+{
+uint8_t x_7; 
+x_7 = lean_string_utf8_at_end(x_1, x_5);
+if (x_7 == 0)
+{
+uint32_t x_8; uint8_t x_9; 
+x_8 = 92;
+x_9 = x_4 == x_8;
+if (x_9 == 0)
+{
+lean_object* x_10; 
+x_10 = lean_string_push(x_3, x_4);
+x_2 = x_5;
+x_3 = x_10;
+goto _start;
+}
+else
+{
+lean_object* x_12; 
+x_12 = l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar(x_1, x_5);
+lean_dec(x_5);
+if (lean_obj_tag(x_12) == 0)
+{
+lean_object* x_13; 
+lean_dec(x_3);
+x_13 = lean_box(0);
+return x_13;
+}
+else
+{
+lean_object* x_14; lean_object* x_15; lean_object* x_16; uint32_t x_17; lean_object* x_18; 
+x_14 = lean_ctor_get(x_12, 0);
+lean_inc(x_14);
+lean_dec(x_12);
+x_15 = lean_ctor_get(x_14, 0);
+lean_inc(x_15);
+x_16 = lean_ctor_get(x_14, 1);
+lean_inc(x_16);
+lean_dec(x_14);
+x_17 = lean_unbox_uint32(x_15);
+lean_dec(x_15);
+x_18 = lean_string_push(x_3, x_17);
+x_2 = x_16;
+x_3 = x_18;
+goto _start;
+}
+}
+}
+else
+{
+lean_object* x_20; 
+lean_dec(x_5);
+lean_dec(x_3);
+x_20 = lean_box(0);
+return x_20;
+}
+}
+else
+{
+lean_object* x_21; 
+lean_dec(x_5);
+x_21 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_21, 0, x_3);
+return x_21;
+}
+}
+}
+}
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit_loop___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit_loop(x_1, x_2, x_3);
+lean_dec(x_1);
+return x_4;
+}
+}
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_2 = lean_unsigned_to_nat(1u);
+x_3 = l_String_splitAux___main___closed__1;
+x_4 = l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit_loop(x_1, x_2, x_3);
+return x_4;
+}
+}
+lean_object* l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
+lean_object* l_Lean_Syntax_isInterpolatedStrLit_x3f_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+lean_dec(x_3);
+x_4 = lean_box(0);
+x_5 = lean_apply_1(x_2, x_4);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_2);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_1(x_3, x_6);
+return x_7;
+}
+}
+}
+lean_object* l_Lean_Syntax_isInterpolatedStrLit_x3f_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Syntax_isInterpolatedStrLit_x3f_match__1___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_Syntax_isInterpolatedStrLit_x3f(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; 
+x_2 = l_Lean_interpolatedStrLitKind;
+x_3 = l_Lean_Syntax_isLit_x3f(x_2, x_1);
+if (lean_obj_tag(x_3) == 0)
+{
+lean_object* x_4; 
+x_4 = lean_box(0);
+return x_4;
+}
+else
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; 
+x_5 = lean_ctor_get(x_3, 0);
+lean_inc(x_5);
+lean_dec(x_3);
+x_6 = lean_unsigned_to_nat(1u);
+x_7 = l_String_splitAux___main___closed__1;
+x_8 = l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrLit_loop(x_5, x_6, x_7);
+lean_dec(x_5);
+return x_8;
+}
+}
+}
+lean_object* l_Lean_Syntax_isInterpolatedStrLit_x3f___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Lean_Syntax_isInterpolatedStrLit_x3f(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
+lean_object* l_Lean_Syntax_expandInterpolatedStrChunks_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+lean_dec(x_3);
+x_4 = lean_box(0);
+x_5 = lean_apply_1(x_2, x_4);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_2);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_1(x_3, x_6);
+return x_7;
+}
+}
+}
+lean_object* l_Lean_Syntax_expandInterpolatedStrChunks_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Syntax_expandInterpolatedStrChunks_match__1___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_expandInterpolatedStrChunks___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
+_start:
+{
+lean_object* x_9; uint8_t x_10; 
+x_9 = lean_array_get_size(x_4);
+x_10 = lean_nat_dec_lt(x_5, x_9);
+lean_dec(x_9);
+if (x_10 == 0)
+{
+lean_object* x_11; 
+lean_dec(x_7);
+lean_dec(x_5);
+lean_dec(x_3);
+lean_dec(x_2);
+x_11 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_11, 0, x_6);
+lean_ctor_set(x_11, 1, x_8);
+return x_11;
+}
+else
+{
+lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
+x_12 = lean_array_fget(x_4, x_5);
+x_13 = lean_unsigned_to_nat(1u);
+x_14 = lean_nat_add(x_5, x_13);
+x_15 = l_Lean_Syntax_isInterpolatedStrLit_x3f(x_12);
+if (lean_obj_tag(x_15) == 0)
+{
+lean_object* x_16; 
+lean_inc(x_3);
+lean_inc(x_7);
+x_16 = lean_apply_3(x_3, x_12, x_7, x_8);
+if (lean_obj_tag(x_16) == 0)
+{
+lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; 
+x_17 = lean_ctor_get(x_16, 0);
+lean_inc(x_17);
+x_18 = lean_ctor_get(x_16, 1);
+lean_inc(x_18);
+lean_dec(x_16);
+x_19 = lean_unsigned_to_nat(0u);
+x_20 = lean_nat_dec_eq(x_5, x_19);
+lean_dec(x_5);
+if (x_20 == 0)
+{
+lean_object* x_21; 
+lean_inc(x_2);
+lean_inc(x_7);
+x_21 = lean_apply_4(x_2, x_6, x_17, x_7, x_18);
+if (lean_obj_tag(x_21) == 0)
+{
+lean_object* x_22; lean_object* x_23; 
+x_22 = lean_ctor_get(x_21, 0);
+lean_inc(x_22);
+x_23 = lean_ctor_get(x_21, 1);
+lean_inc(x_23);
+lean_dec(x_21);
+x_5 = x_14;
+x_6 = x_22;
+x_8 = x_23;
+goto _start;
+}
+else
+{
+uint8_t x_25; 
+lean_dec(x_14);
+lean_dec(x_7);
+lean_dec(x_3);
+lean_dec(x_2);
+x_25 = !lean_is_exclusive(x_21);
+if (x_25 == 0)
+{
+return x_21;
+}
+else
+{
+lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_26 = lean_ctor_get(x_21, 0);
+x_27 = lean_ctor_get(x_21, 1);
+lean_inc(x_27);
+lean_inc(x_26);
+lean_dec(x_21);
+x_28 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_28, 0, x_26);
+lean_ctor_set(x_28, 1, x_27);
+return x_28;
+}
+}
+}
+else
+{
+lean_dec(x_6);
+x_5 = x_14;
+x_6 = x_17;
+x_8 = x_18;
+goto _start;
+}
+}
+else
+{
+uint8_t x_30; 
+lean_dec(x_14);
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_3);
+lean_dec(x_2);
+x_30 = !lean_is_exclusive(x_16);
+if (x_30 == 0)
+{
+return x_16;
+}
+else
+{
+lean_object* x_31; lean_object* x_32; lean_object* x_33; 
+x_31 = lean_ctor_get(x_16, 0);
+x_32 = lean_ctor_get(x_16, 1);
+lean_inc(x_32);
+lean_inc(x_31);
+lean_dec(x_16);
+x_33 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_33, 0, x_31);
+lean_ctor_set(x_33, 1, x_32);
+return x_33;
+}
+}
+}
+else
+{
+lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; 
+lean_dec(x_12);
+x_34 = lean_ctor_get(x_15, 0);
+lean_inc(x_34);
+lean_dec(x_15);
+x_35 = l_Lean_SourceInfo_inhabited___closed__1;
+x_36 = l_Lean_mkStxStrLit(x_34, x_35);
+lean_inc(x_3);
+lean_inc(x_7);
+x_37 = lean_apply_3(x_3, x_36, x_7, x_8);
+if (lean_obj_tag(x_37) == 0)
+{
+lean_object* x_38; lean_object* x_39; lean_object* x_40; uint8_t x_41; 
+x_38 = lean_ctor_get(x_37, 0);
+lean_inc(x_38);
+x_39 = lean_ctor_get(x_37, 1);
+lean_inc(x_39);
+lean_dec(x_37);
+x_40 = lean_unsigned_to_nat(0u);
+x_41 = lean_nat_dec_eq(x_5, x_40);
+lean_dec(x_5);
+if (x_41 == 0)
+{
+lean_object* x_42; 
+lean_inc(x_2);
+lean_inc(x_7);
+x_42 = lean_apply_4(x_2, x_6, x_38, x_7, x_39);
+if (lean_obj_tag(x_42) == 0)
+{
+lean_object* x_43; lean_object* x_44; 
+x_43 = lean_ctor_get(x_42, 0);
+lean_inc(x_43);
+x_44 = lean_ctor_get(x_42, 1);
+lean_inc(x_44);
+lean_dec(x_42);
+x_5 = x_14;
+x_6 = x_43;
+x_8 = x_44;
+goto _start;
+}
+else
+{
+uint8_t x_46; 
+lean_dec(x_14);
+lean_dec(x_7);
+lean_dec(x_3);
+lean_dec(x_2);
+x_46 = !lean_is_exclusive(x_42);
+if (x_46 == 0)
+{
+return x_42;
+}
+else
+{
+lean_object* x_47; lean_object* x_48; lean_object* x_49; 
+x_47 = lean_ctor_get(x_42, 0);
+x_48 = lean_ctor_get(x_42, 1);
+lean_inc(x_48);
+lean_inc(x_47);
+lean_dec(x_42);
+x_49 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_49, 0, x_47);
+lean_ctor_set(x_49, 1, x_48);
+return x_49;
+}
+}
+}
+else
+{
+lean_dec(x_6);
+x_5 = x_14;
+x_6 = x_38;
+x_8 = x_39;
+goto _start;
+}
+}
+else
+{
+uint8_t x_51; 
+lean_dec(x_14);
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_3);
+lean_dec(x_2);
+x_51 = !lean_is_exclusive(x_37);
+if (x_51 == 0)
+{
+return x_37;
+}
+else
+{
+lean_object* x_52; lean_object* x_53; lean_object* x_54; 
+x_52 = lean_ctor_get(x_37, 0);
+x_53 = lean_ctor_get(x_37, 1);
+lean_inc(x_53);
+lean_inc(x_52);
+lean_dec(x_37);
+x_54 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_54, 0, x_52);
+lean_ctor_set(x_54, 1, x_53);
+return x_54;
+}
+}
+}
+}
+}
+}
+lean_object* l_Lean_Syntax_expandInterpolatedStrChunks(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; 
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = lean_box(0);
+x_8 = l_Array_iterateMAux___main___at_Lean_Syntax_expandInterpolatedStrChunks___spec__1(x_1, x_2, x_3, x_1, x_6, x_7, x_4, x_5);
+return x_8;
+}
+}
+lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_expandInterpolatedStrChunks___spec__1___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, lean_object* x_8) {
+_start:
+{
+lean_object* x_9; 
+x_9 = l_Array_iterateMAux___main___at_Lean_Syntax_expandInterpolatedStrChunks___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
+lean_dec(x_4);
+lean_dec(x_1);
+return x_9;
+}
+}
+lean_object* l_Lean_Syntax_expandInterpolatedStrChunks___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+lean_object* x_6; 
+x_6 = l_Lean_Syntax_expandInterpolatedStrChunks(x_1, x_2, x_3, x_4, x_5);
+lean_dec(x_1);
+return x_6;
+}
+}
 lean_object* initialize_Init_Data_Option_BasicAux(lean_object*);
 lean_object* initialize_Init_Data_String_Basic(lean_object*);
 lean_object* initialize_Init_Data_Array_Basic(lean_object*);
@@ -8362,6 +9062,18 @@ l_Lean_fieldIdxKind___closed__2 = _init_l_Lean_fieldIdxKind___closed__2();
 lean_mark_persistent(l_Lean_fieldIdxKind___closed__2);
 l_Lean_fieldIdxKind = _init_l_Lean_fieldIdxKind();
 lean_mark_persistent(l_Lean_fieldIdxKind);
+l_Lean_interpolatedStrLitKind___closed__1 = _init_l_Lean_interpolatedStrLitKind___closed__1();
+lean_mark_persistent(l_Lean_interpolatedStrLitKind___closed__1);
+l_Lean_interpolatedStrLitKind___closed__2 = _init_l_Lean_interpolatedStrLitKind___closed__2();
+lean_mark_persistent(l_Lean_interpolatedStrLitKind___closed__2);
+l_Lean_interpolatedStrLitKind = _init_l_Lean_interpolatedStrLitKind();
+lean_mark_persistent(l_Lean_interpolatedStrLitKind);
+l_Lean_interpolatedStrKind___closed__1 = _init_l_Lean_interpolatedStrKind___closed__1();
+lean_mark_persistent(l_Lean_interpolatedStrKind___closed__1);
+l_Lean_interpolatedStrKind___closed__2 = _init_l_Lean_interpolatedStrKind___closed__2();
+lean_mark_persistent(l_Lean_interpolatedStrKind___closed__2);
+l_Lean_interpolatedStrKind = _init_l_Lean_interpolatedStrKind();
+lean_mark_persistent(l_Lean_interpolatedStrKind);
 l_Lean_Syntax_getKind___closed__1 = _init_l_Lean_Syntax_getKind___closed__1();
 lean_mark_persistent(l_Lean_Syntax_getKind___closed__1);
 l_Lean_Syntax_getKind___closed__2 = _init_l_Lean_Syntax_getKind___closed__2();
@@ -8518,6 +9230,8 @@ l___private_Init_LeanInit_15__quoteOption___rarg___closed__5 = _init_l___private
 lean_mark_persistent(l___private_Init_LeanInit_15__quoteOption___rarg___closed__5);
 l___private_Init_LeanInit_15__quoteOption___rarg___closed__6 = _init_l___private_Init_LeanInit_15__quoteOption___rarg___closed__6();
 lean_mark_persistent(l___private_Init_LeanInit_15__quoteOption___rarg___closed__6);
+l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar___boxed__const__1 = _init_l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar___boxed__const__1();
+lean_mark_persistent(l___private_Init_LeanInit_0__Lean_Syntax_decodeInterpStrQuotedChar___boxed__const__1);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Lean/Elab/Quotation.c

@@ -89,6 +89,7 @@ lean_object* l_ReaderT_pure___at_Lean_Elab_Term_Quotation_HeadInfo_Inhabited___s
 lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuot___closed__1;
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__34;
 lean_object* l___private_Lean_Elab_Quotation_11__oldRunTermElabMUnsafe___rarg(lean_object*, lean_object*);
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__3;
 lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__9;
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__48;
 lean_object* l_List_mapM___main___at___private_Lean_Elab_Quotation_6__compileStxMatch___main___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -391,6 +392,7 @@ lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__25;
 extern lean_object* l_Lean_Elab_Term_termElabAttribute;
 lean_object* l___private_Lean_Elab_Quotation_5__explodeHeadPat___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_mkAppStx___closed__3;
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot(lean_object*);
 lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__29;
 lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__4;
 lean_object* l_Lean_KVMap_setName(lean_object*, lean_object*, lean_object*);
@@ -487,6 +489,7 @@ lean_object* l_List_filterAux___main___at___private_Lean_Elab_Quotation_6__compi
 lean_object* l_List_foldl___main___at___private_Lean_Elab_Quotation_6__compileStxMatch___main___spec__3___boxed(lean_object*, lean_object*);
 lean_object* l_List_map___main___at___private_Lean_Elab_Quotation_6__compileStxMatch___main___spec__7(lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__54;
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__4;
 extern lean_object* l_Lean_Unhygienic_MonadQuotation___closed__2;
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__62;
 extern lean_object* l_Lean_TraceState_Inhabited___closed__1;
@@ -509,8 +512,11 @@ lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__16;
 lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___closed__4;
 lean_object* l_Lean_Elab_Term_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_filterAux___main___at___private_Lean_Elab_Quotation_6__compileStxMatch___main___spec__9___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_Quotation_elabDoElemQuot(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__63;
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__1;
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__7;
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__2;
 extern lean_object* l_Lean_Prod_hasQuote___rarg___closed__4;
 lean_object* l_List_mapM___main___at___private_Lean_Elab_Quotation_6__compileStxMatch___main___spec__8___closed__8;
 lean_object* l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__20;
@@ -4387,6 +4393,62 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
+lean_object* l_Lean_Elab_Term_Quotation_elabDoElemQuot(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+_start:
+{
+lean_object* x_10; lean_object* x_11; 
+x_10 = l_Lean_Elab_Term_Quotation_elabLevelQuot___closed__1;
+x_11 = l_Lean_Elab_Term_adaptExpander(x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
+return x_11;
+}
+}
+lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("doElem");
+return x_1;
+}
+}
+lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_mkAppStx___closed__6;
+x_2 = l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__2;
+x_2 = l_Lean_Syntax_isQuot___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__4() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Quotation_elabDoElemQuot), 9, 0);
+return x_1;
+}
+}
+lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Elab_Term_termElabAttribute;
+x_3 = l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__3;
+x_4 = l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__4;
+x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
 lean_object* l_ReaderT_pure___at_Lean_Elab_Term_Quotation_HeadInfo_Inhabited___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, lean_object* x_7, lean_object* x_8) {
 _start:
 {
@@ -23894,6 +23956,17 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabStxQuot___close
 res = l___regBuiltin_Lean_Elab_Term_Quotation_elabStxQuot(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__1();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__1);
+l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__2();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__2);
+l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__3 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__3();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__3);
+l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__4 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__4();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot___closed__4);
+res = l___regBuiltin_Lean_Elab_Term_Quotation_elabDoElemQuot(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 l_Lean_Elab_Term_Quotation_HeadInfo_Inhabited___closed__1 = _init_l_Lean_Elab_Term_Quotation_HeadInfo_Inhabited___closed__1();
 lean_mark_persistent(l_Lean_Elab_Term_Quotation_HeadInfo_Inhabited___closed__1);
 l_Lean_Elab_Term_Quotation_HeadInfo_Inhabited___closed__2 = _init_l_Lean_Elab_Term_Quotation_HeadInfo_Inhabited___closed__2();

stage0/stdlib/Lean/Parser/StrInterpolation.c

@@ -0,0 +1,697 @@
+// Lean compiler output
+// Module: Lean.Parser.StrInterpolation
+// Imports: Init Lean.Parser.Basic
+#include <lean/lean.h>
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+lean_object* l_Lean_Parser_quotedCharCoreFn___at_Lean_Parser_interpolatedStrFn_parse___spec__2___boxed(lean_object*, lean_object*);
+uint8_t l_Lean_Parser_isQuotableCharDefault(uint32_t);
+lean_object* l_Lean_Parser_ParserState_next(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_interpolatedStrNoAntiquot___closed__1;
+lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
+lean_object* lean_array_get_size(lean_object*);
+extern lean_object* l_Lean_interpolatedStrKind;
+lean_object* l_Lean_Parser_mkAtomicInfo(lean_object*);
+lean_object* l_Lean_Parser_mkNodeToken(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_string_utf8_next(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_interpolatedStr___elambda__1___closed__1;
+lean_object* l_Lean_Parser_interpolatedStr___elambda__1___closed__2;
+lean_object* l_Lean_Parser_ParserState_setPos(lean_object*, lean_object*);
+uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_interpolatedStrFn_parse___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_interpolatedStrFn_parse___closed__1;
+lean_object* l_Lean_Parser_interpolatedStrNoAntiquot(lean_object*);
+uint8_t l_Lean_Parser_tryAnti(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_orelseInfo(lean_object*, lean_object*);
+uint8_t l_Lean_Parser_isQuotableCharForStrInterpolant(uint32_t);
+extern lean_object* l_Lean_Parser_ParserState_mkEOIError___closed__1;
+uint32_t lean_string_utf8_get(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_interpolatedStr(lean_object*);
+lean_object* l_Lean_Parser_quotedCharCoreFn___at_Lean_Parser_interpolatedStrFn_parse___spec__2(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_interpolatedStr___closed__1;
+extern lean_object* l_Lean_Parser_quotedCharCoreFn___closed__1;
+lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*);
+uint8_t l_UInt32_decEq(uint32_t, uint32_t);
+lean_object* l_Lean_Parser_hexDigitFn(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_mergeOrElseErrors(lean_object*, lean_object*, lean_object*, uint8_t);
+lean_object* l_Lean_Parser_interpolatedStr___elambda__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_satisfyFn___at_Lean_Parser_interpolatedStrFn_parse___spec__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_interpolatedStrFn_parse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_interpolatedStrNoAntiquot___closed__2;
+lean_object* l_Lean_Parser_satisfyFn___at_Lean_Parser_interpolatedStrFn_parse___spec__1___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
+lean_object* l_Lean_Parser_isQuotableCharForStrInterpolant___boxed(lean_object*);
+lean_object* l_Lean_Parser_interpolatedStrFn(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_ParserState_mkUnexpectedError(lean_object*, lean_object*);
+uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
+extern lean_object* l_Lean_interpolatedStrLitKind;
+uint8_t l_Lean_Parser_isQuotableCharForStrInterpolant(uint32_t x_1) {
+_start:
+{
+uint32_t x_2; uint8_t x_3; 
+x_2 = 123;
+x_3 = x_1 == x_2;
+if (x_3 == 0)
+{
+uint8_t x_4; 
+x_4 = l_Lean_Parser_isQuotableCharDefault(x_1);
+return x_4;
+}
+else
+{
+uint8_t x_5; 
+x_5 = 1;
+return x_5;
+}
+}
+}
+lean_object* l_Lean_Parser_isQuotableCharForStrInterpolant___boxed(lean_object* x_1) {
+_start:
+{
+uint32_t x_2; uint8_t x_3; lean_object* x_4; 
+x_2 = lean_unbox_uint32(x_1);
+lean_dec(x_1);
+x_3 = l_Lean_Parser_isQuotableCharForStrInterpolant(x_2);
+x_4 = lean_box(x_3);
+return x_4;
+}
+}
+lean_object* l_Lean_Parser_satisfyFn___at_Lean_Parser_interpolatedStrFn_parse___spec__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; uint8_t x_7; 
+x_4 = lean_ctor_get(x_3, 1);
+lean_inc(x_4);
+x_5 = lean_ctor_get(x_2, 0);
+x_6 = lean_ctor_get(x_5, 0);
+x_7 = lean_string_utf8_at_end(x_6, x_4);
+if (x_7 == 0)
+{
+uint32_t x_8; uint32_t x_9; uint8_t x_10; 
+x_8 = lean_string_utf8_get(x_6, x_4);
+x_9 = 125;
+x_10 = x_8 == x_9;
+if (x_10 == 0)
+{
+lean_object* x_11; 
+lean_dec(x_4);
+x_11 = l_Lean_Parser_ParserState_mkUnexpectedError(x_3, x_1);
+return x_11;
+}
+else
+{
+lean_object* x_12; 
+lean_dec(x_1);
+x_12 = l_Lean_Parser_ParserState_next(x_3, x_6, x_4);
+lean_dec(x_4);
+return x_12;
+}
+}
+else
+{
+lean_object* x_13; lean_object* x_14; 
+lean_dec(x_4);
+lean_dec(x_1);
+x_13 = l_Lean_Parser_ParserState_mkEOIError___closed__1;
+x_14 = l_Lean_Parser_ParserState_mkUnexpectedError(x_3, x_13);
+return x_14;
+}
+}
+}
+lean_object* l_Lean_Parser_quotedCharCoreFn___at_Lean_Parser_interpolatedStrFn_parse___spec__2(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; 
+x_3 = lean_ctor_get(x_1, 0);
+x_4 = lean_ctor_get(x_3, 0);
+x_5 = lean_ctor_get(x_2, 1);
+lean_inc(x_5);
+x_6 = lean_string_utf8_at_end(x_4, x_5);
+if (x_6 == 0)
+{
+uint32_t x_7; uint8_t x_8; 
+x_7 = lean_string_utf8_get(x_4, x_5);
+x_8 = l_Lean_Parser_isQuotableCharForStrInterpolant(x_7);
+if (x_8 == 0)
+{
+uint32_t x_9; uint8_t x_10; uint8_t x_28; 
+x_9 = 120;
+x_28 = x_7 == x_9;
+if (x_28 == 0)
+{
+uint8_t x_29; 
+x_29 = 0;
+x_10 = x_29;
+goto block_27;
+}
+else
+{
+uint8_t x_30; 
+x_30 = 1;
+x_10 = x_30;
+goto block_27;
+}
+block_27:
+{
+if (x_10 == 0)
+{
+uint32_t x_11; uint8_t x_12; 
+x_11 = 117;
+x_12 = x_7 == x_11;
+if (x_12 == 0)
+{
+lean_object* x_13; lean_object* x_14; 
+lean_dec(x_5);
+x_13 = l_Lean_Parser_quotedCharCoreFn___closed__1;
+x_14 = l_Lean_Parser_ParserState_mkUnexpectedError(x_2, x_13);
+return x_14;
+}
+else
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_15 = l_Lean_Parser_ParserState_next(x_2, x_4, x_5);
+lean_dec(x_5);
+x_16 = l_Lean_Parser_hexDigitFn(x_1, x_15);
+x_17 = lean_ctor_get(x_16, 3);
+lean_inc(x_17);
+if (lean_obj_tag(x_17) == 0)
+{
+lean_object* x_18; lean_object* x_19; 
+x_18 = l_Lean_Parser_hexDigitFn(x_1, x_16);
+x_19 = lean_ctor_get(x_18, 3);
+lean_inc(x_19);
+if (lean_obj_tag(x_19) == 0)
+{
+lean_object* x_20; lean_object* x_21; 
+x_20 = l_Lean_Parser_hexDigitFn(x_1, x_18);
+x_21 = lean_ctor_get(x_20, 3);
+lean_inc(x_21);
+if (lean_obj_tag(x_21) == 0)
+{
+lean_object* x_22; 
+x_22 = l_Lean_Parser_hexDigitFn(x_1, x_20);
+return x_22;
+}
+else
+{
+lean_dec(x_21);
+return x_20;
+}
+}
+else
+{
+lean_dec(x_19);
+return x_18;
+}
+}
+else
+{
+lean_dec(x_17);
+return x_16;
+}
+}
+}
+else
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; 
+x_23 = l_Lean_Parser_ParserState_next(x_2, x_4, x_5);
+lean_dec(x_5);
+x_24 = l_Lean_Parser_hexDigitFn(x_1, x_23);
+x_25 = lean_ctor_get(x_24, 3);
+lean_inc(x_25);
+if (lean_obj_tag(x_25) == 0)
+{
+lean_object* x_26; 
+x_26 = l_Lean_Parser_hexDigitFn(x_1, x_24);
+return x_26;
+}
+else
+{
+lean_dec(x_25);
+return x_24;
+}
+}
+}
+}
+else
+{
+lean_object* x_31; 
+x_31 = l_Lean_Parser_ParserState_next(x_2, x_4, x_5);
+lean_dec(x_5);
+return x_31;
+}
+}
+else
+{
+lean_object* x_32; lean_object* x_33; 
+lean_dec(x_5);
+x_32 = l_Lean_Parser_ParserState_mkEOIError___closed__1;
+x_33 = l_Lean_Parser_ParserState_mkUnexpectedError(x_2, x_32);
+return x_33;
+}
+}
+}
+lean_object* _init_l_Lean_Parser_interpolatedStrFn_parse___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("expected '}'");
+return x_1;
+}
+}
+lean_object* l_Lean_Parser_interpolatedStrFn_parse(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_ctor_get(x_6, 1);
+lean_inc(x_7);
+x_8 = lean_string_utf8_at_end(x_2, x_7);
+if (x_8 == 0)
+{
+uint32_t x_9; lean_object* x_10; lean_object* x_11; uint32_t x_12; uint8_t x_13; uint8_t x_44; 
+x_9 = lean_string_utf8_get(x_2, x_7);
+x_10 = lean_string_utf8_next(x_2, x_7);
+lean_dec(x_7);
+x_11 = l_Lean_Parser_ParserState_setPos(x_6, x_10);
+x_12 = 34;
+x_44 = x_9 == x_12;
+if (x_44 == 0)
+{
+uint8_t x_45; 
+x_45 = 0;
+x_13 = x_45;
+goto block_43;
+}
+else
+{
+uint8_t x_46; 
+x_46 = 1;
+x_13 = x_46;
+goto block_43;
+}
+block_43:
+{
+if (x_13 == 0)
+{
+uint32_t x_14; uint8_t x_15; uint8_t x_36; 
+x_14 = 92;
+x_36 = x_9 == x_14;
+if (x_36 == 0)
+{
+uint8_t x_37; 
+x_37 = 0;
+x_15 = x_37;
+goto block_35;
+}
+else
+{
+uint8_t x_38; 
+x_38 = 1;
+x_15 = x_38;
+goto block_35;
+}
+block_35:
+{
+if (x_15 == 0)
+{
+uint32_t x_16; uint8_t x_17; uint8_t x_29; 
+x_16 = 123;
+x_29 = x_9 == x_16;
+if (x_29 == 0)
+{
+uint8_t x_30; 
+x_30 = 0;
+x_17 = x_30;
+goto block_28;
+}
+else
+{
+uint8_t x_31; 
+x_31 = 1;
+x_17 = x_31;
+goto block_28;
+}
+block_28:
+{
+if (x_17 == 0)
+{
+x_6 = x_11;
+goto _start;
+}
+else
+{
+lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+x_19 = l_Lean_interpolatedStrLitKind;
+x_20 = l_Lean_Parser_mkNodeToken(x_19, x_4, x_5, x_11);
+lean_inc(x_1);
+lean_inc(x_5);
+x_21 = lean_apply_2(x_1, x_5, x_20);
+x_22 = lean_ctor_get(x_21, 3);
+lean_inc(x_22);
+if (lean_obj_tag(x_22) == 0)
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
+x_23 = lean_ctor_get(x_21, 1);
+lean_inc(x_23);
+x_24 = l_Lean_Parser_interpolatedStrFn_parse___closed__1;
+x_25 = l_Lean_Parser_satisfyFn___at_Lean_Parser_interpolatedStrFn_parse___spec__1(x_24, x_5, x_21);
+x_26 = lean_ctor_get(x_25, 3);
+lean_inc(x_26);
+if (lean_obj_tag(x_26) == 0)
+{
+x_4 = x_23;
+x_6 = x_25;
+goto _start;
+}
+else
+{
+lean_dec(x_26);
+lean_dec(x_23);
+lean_dec(x_5);
+lean_dec(x_3);
+lean_dec(x_1);
+return x_25;
+}
+}
+else
+{
+lean_dec(x_22);
+lean_dec(x_5);
+lean_dec(x_3);
+lean_dec(x_1);
+return x_21;
+}
+}
+}
+}
+else
+{
+lean_object* x_32; lean_object* x_33; 
+x_32 = l_Lean_Parser_quotedCharCoreFn___at_Lean_Parser_interpolatedStrFn_parse___spec__2(x_5, x_11);
+x_33 = lean_ctor_get(x_32, 3);
+lean_inc(x_33);
+if (lean_obj_tag(x_33) == 0)
+{
+x_6 = x_32;
+goto _start;
+}
+else
+{
+lean_dec(x_33);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_1);
+return x_32;
+}
+}
+}
+}
+else
+{
+lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; 
+lean_dec(x_1);
+x_39 = l_Lean_interpolatedStrLitKind;
+x_40 = l_Lean_Parser_mkNodeToken(x_39, x_4, x_5, x_11);
+lean_dec(x_5);
+x_41 = l_Lean_interpolatedStrKind;
+x_42 = l_Lean_Parser_ParserState_mkNode(x_40, x_41, x_3);
+return x_42;
+}
+}
+}
+else
+{
+lean_object* x_47; lean_object* x_48; 
+lean_dec(x_7);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_1);
+x_47 = l_Lean_Parser_ParserState_mkEOIError___closed__1;
+x_48 = l_Lean_Parser_ParserState_mkUnexpectedError(x_6, x_47);
+return x_48;
+}
+}
+}
+lean_object* l_Lean_Parser_satisfyFn___at_Lean_Parser_interpolatedStrFn_parse___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_Parser_satisfyFn___at_Lean_Parser_interpolatedStrFn_parse___spec__1(x_1, x_2, x_3);
+lean_dec(x_2);
+return x_4;
+}
+}
+lean_object* l_Lean_Parser_quotedCharCoreFn___at_Lean_Parser_interpolatedStrFn_parse___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Parser_quotedCharCoreFn___at_Lean_Parser_interpolatedStrFn_parse___spec__2(x_1, x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
+lean_object* l_Lean_Parser_interpolatedStrFn_parse___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_Lean_Parser_interpolatedStrFn_parse(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_2);
+return x_7;
+}
+}
+lean_object* l_Lean_Parser_interpolatedStrFn(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; uint8_t x_9; 
+x_4 = lean_ctor_get(x_2, 0);
+lean_inc(x_4);
+x_5 = lean_ctor_get(x_4, 0);
+lean_inc(x_5);
+lean_dec(x_4);
+x_6 = lean_ctor_get(x_3, 0);
+lean_inc(x_6);
+x_7 = lean_array_get_size(x_6);
+lean_dec(x_6);
+x_8 = lean_ctor_get(x_3, 1);
+lean_inc(x_8);
+x_9 = lean_string_utf8_at_end(x_5, x_8);
+if (x_9 == 0)
+{
+lean_object* x_10; lean_object* x_11; 
+x_10 = l_Lean_Parser_ParserState_next(x_3, x_5, x_8);
+x_11 = l_Lean_Parser_interpolatedStrFn_parse(x_1, x_5, x_7, x_8, x_2, x_10);
+lean_dec(x_5);
+return x_11;
+}
+else
+{
+lean_object* x_12; lean_object* x_13; 
+lean_dec(x_8);
+lean_dec(x_7);
+lean_dec(x_5);
+lean_dec(x_2);
+lean_dec(x_1);
+x_12 = l_Lean_Parser_ParserState_mkEOIError___closed__1;
+x_13 = l_Lean_Parser_ParserState_mkUnexpectedError(x_3, x_12);
+return x_13;
+}
+}
+}
+lean_object* _init_l_Lean_Parser_interpolatedStrNoAntiquot___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("interpolatedStr");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Parser_interpolatedStrNoAntiquot___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Parser_interpolatedStrNoAntiquot___closed__1;
+x_2 = l_Lean_Parser_mkAtomicInfo(x_1);
+return x_2;
+}
+}
+lean_object* l_Lean_Parser_interpolatedStrNoAntiquot(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = lean_ctor_get(x_1, 1);
+lean_inc(x_2);
+lean_dec(x_1);
+x_3 = lean_alloc_closure((void*)(l_Lean_Parser_interpolatedStrFn), 3, 1);
+lean_closure_set(x_3, 0, x_2);
+x_4 = l_Lean_Parser_interpolatedStrNoAntiquot___closed__2;
+x_5 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_5, 0, x_4);
+lean_ctor_set(x_5, 1, x_3);
+return x_5;
+}
+}
+lean_object* _init_l_Lean_Parser_interpolatedStr___elambda__1___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_interpolatedStrKind;
+x_2 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_Parser_interpolatedStr___elambda__1___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; 
+x_1 = l_Lean_Parser_interpolatedStrNoAntiquot___closed__1;
+x_2 = l_Lean_Parser_interpolatedStr___elambda__1___closed__1;
+x_3 = 1;
+x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
+return x_4;
+}
+}
+lean_object* l_Lean_Parser_interpolatedStr___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; lean_object* x_5; uint8_t x_6; 
+x_4 = l_Lean_Parser_interpolatedStr___elambda__1___closed__2;
+x_5 = lean_ctor_get(x_4, 1);
+lean_inc(x_5);
+lean_inc(x_3);
+lean_inc(x_2);
+x_6 = l_Lean_Parser_tryAnti(x_2, x_3);
+if (x_6 == 0)
+{
+lean_object* x_7; 
+lean_dec(x_5);
+x_7 = lean_apply_2(x_1, x_2, x_3);
+return x_7;
+}
+else
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_8 = lean_ctor_get(x_3, 0);
+lean_inc(x_8);
+x_9 = lean_array_get_size(x_8);
+lean_dec(x_8);
+x_10 = lean_ctor_get(x_3, 1);
+lean_inc(x_10);
+lean_inc(x_2);
+x_11 = lean_apply_2(x_5, x_2, x_3);
+x_12 = lean_ctor_get(x_11, 3);
+lean_inc(x_12);
+if (lean_obj_tag(x_12) == 0)
+{
+lean_dec(x_10);
+lean_dec(x_9);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_11;
+}
+else
+{
+lean_object* x_13; lean_object* x_14; uint8_t x_15; 
+x_13 = lean_ctor_get(x_12, 0);
+lean_inc(x_13);
+lean_dec(x_12);
+x_14 = lean_ctor_get(x_11, 1);
+lean_inc(x_14);
+x_15 = lean_nat_dec_eq(x_14, x_10);
+lean_dec(x_14);
+if (x_15 == 0)
+{
+lean_dec(x_13);
+lean_dec(x_10);
+lean_dec(x_9);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_11;
+}
+else
+{
+lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19; 
+lean_inc(x_10);
+x_16 = l_Lean_Parser_ParserState_restore(x_11, x_9, x_10);
+lean_dec(x_9);
+x_17 = lean_apply_2(x_1, x_2, x_16);
+x_18 = 1;
+x_19 = l_Lean_Parser_mergeOrElseErrors(x_17, x_13, x_10, x_18);
+lean_dec(x_10);
+return x_19;
+}
+}
+}
+}
+}
+lean_object* _init_l_Lean_Parser_interpolatedStr___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_Parser_interpolatedStr___elambda__1___closed__2;
+x_2 = lean_ctor_get(x_1, 0);
+lean_inc(x_2);
+x_3 = l_Lean_Parser_interpolatedStrNoAntiquot___closed__2;
+x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
+return x_4;
+}
+}
+lean_object* l_Lean_Parser_interpolatedStr(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 = lean_ctor_get(x_1, 1);
+lean_inc(x_2);
+lean_dec(x_1);
+x_3 = lean_alloc_closure((void*)(l_Lean_Parser_interpolatedStrFn), 3, 1);
+lean_closure_set(x_3, 0, x_2);
+x_4 = lean_alloc_closure((void*)(l_Lean_Parser_interpolatedStr___elambda__1), 3, 1);
+lean_closure_set(x_4, 0, x_3);
+x_5 = l_Lean_Parser_interpolatedStr___closed__1;
+x_6 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_6, 0, x_5);
+lean_ctor_set(x_6, 1, x_4);
+return x_6;
+}
+}
+lean_object* initialize_Init(lean_object*);
+lean_object* initialize_Lean_Parser_Basic(lean_object*);
+static bool _G_initialized = false;
+lean_object* initialize_Lean_Parser_StrInterpolation(lean_object* w) {
+lean_object * res;
+if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
+_G_initialized = true;
+res = initialize_Init(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Parser_Basic(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_Lean_Parser_interpolatedStrFn_parse___closed__1 = _init_l_Lean_Parser_interpolatedStrFn_parse___closed__1();
+lean_mark_persistent(l_Lean_Parser_interpolatedStrFn_parse___closed__1);
+l_Lean_Parser_interpolatedStrNoAntiquot___closed__1 = _init_l_Lean_Parser_interpolatedStrNoAntiquot___closed__1();
+lean_mark_persistent(l_Lean_Parser_interpolatedStrNoAntiquot___closed__1);
+l_Lean_Parser_interpolatedStrNoAntiquot___closed__2 = _init_l_Lean_Parser_interpolatedStrNoAntiquot___closed__2();
+lean_mark_persistent(l_Lean_Parser_interpolatedStrNoAntiquot___closed__2);
+l_Lean_Parser_interpolatedStr___elambda__1___closed__1 = _init_l_Lean_Parser_interpolatedStr___elambda__1___closed__1();
+lean_mark_persistent(l_Lean_Parser_interpolatedStr___elambda__1___closed__1);
+l_Lean_Parser_interpolatedStr___elambda__1___closed__2 = _init_l_Lean_Parser_interpolatedStr___elambda__1___closed__2();
+lean_mark_persistent(l_Lean_Parser_interpolatedStr___elambda__1___closed__2);
+l_Lean_Parser_interpolatedStr___closed__1 = _init_l_Lean_Parser_interpolatedStr___closed__1();
+lean_mark_persistent(l_Lean_Parser_interpolatedStr___closed__1);
+return lean_io_result_mk_ok(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif

stage0/stdlib/Lean/PrettyPrinter/Formatter.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.PrettyPrinter.Formatter
-// Imports: Init Lean.CoreM Lean.Parser.Extension Lean.KeyedDeclsAttribute Lean.ParserCompiler.Attribute Lean.PrettyPrinter.Backtrack
+// Imports: Init Lean.CoreM Lean.Parser.Extension Lean.Parser.StrInterpolation Lean.KeyedDeclsAttribute Lean.ParserCompiler.Attribute Lean.PrettyPrinter.Backtrack
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -120,6 +120,7 @@ lean_object* l_Lean_PrettyPrinter_Formatter_checkKind___lambda__1___closed__2;
 lean_object* l_Lean_PrettyPrinter_Formatter_checkStackTop_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_symbolNoWs_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_nameLitKind;
+lean_object* l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__3;
 lean_object* l_Substring_takeRightWhileAux___main___at_Lean_PrettyPrinter_Formatter_pushTokenCore___spec__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_throwError___at_Lean_PrettyPrinter_Formatter_formatterForKind___spec__1(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_notFollowedBy_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -140,6 +141,7 @@ lean_object* l_Lean_PrettyPrinter_Formatter_checkColGe_formatter___boxed(lean_ob
 lean_object* l_Lean_PrettyPrinter_Formatter_formatterForKind(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_withAntiquot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_isEqvAux___main___at_Lean_PrettyPrinter_Formatter_identNoAntiquot_formatter___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_MonadTraverser_getCur___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_forMAux___main___at_Lean_PrettyPrinter_Formatter_many_formatter___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_String_trimRight(lean_object*);
@@ -179,6 +181,7 @@ lean_object* l_Lean_PrettyPrinter_Formatter_checkKind___lambda__1___closed__6;
 lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___closed__5;
 lean_object* l_Lean_PrettyPrinter_Formatter_symbol_formatter___lambda__1___closed__4;
 lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___closed__3;
+lean_object* l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___boxed(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_toggleInsideQuot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_node_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_unicodeSymbol_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -334,6 +337,7 @@ lean_object* l_Lean_PrettyPrinter_Formatter_throwBacktrack___rarg___closed__1;
 lean_object* l_Lean_PrettyPrinter_Formatter_concat___closed__1;
 lean_object* l_Lean_PrettyPrinter_Formatter_setStack(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_throwError___at_Lean_addAttribute___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__2;
 lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_back___at_Lean_PrettyPrinter_Formatter_indent___spec__1(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_FormatterM_monadTraverser___closed__5;
@@ -345,6 +349,7 @@ lean_object* l_Lean_PrettyPrinter_mkCombinatorFormatterAttribute___closed__3;
 lean_object* l_Lean_PrettyPrinter_Formatter_pushTokenCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_foldr___main___at_Lean_PrettyPrinter_Formatter_identNoAntiquot_formatter___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_checkKind___closed__3;
+lean_object* l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___closed__7;
 extern lean_object* l_PUnit_Inhabited;
 lean_object* l_Lean_PrettyPrinter_Formatter_quotedSymbol_formatter___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -375,6 +380,7 @@ lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 extern lean_object* l_Lean_mkOptionalNode___closed__2;
 lean_object* lean_nat_mod(lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_FormatterM_monadTraverser___closed__1;
+lean_object* l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_symbol_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_simp_macro_scopes(lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___closed__2;
@@ -409,6 +415,7 @@ lean_object* l_List_forM___main___at_Lean_PrettyPrinter_Formatter_sepBy_formatte
 lean_object* l_Lean_PrettyPrinter_Formatter_group(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_format___closed__2;
 lean_object* l_Lean_PrettyPrinter_Formatter_checkKind___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__1;
 lean_object* l_Lean_PrettyPrinter_Formatter_withoutPosition_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_to_int(lean_object*);
 uint8_t l_Lean_Syntax_isToken(lean_object*, lean_object*);
@@ -3264,7 +3271,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___lambda__1___closed__1;
-x_2 = lean_unsigned_to_nat(184u);
+x_2 = lean_unsigned_to_nat(185u);
 x_3 = lean_unsigned_to_nat(6u);
 x_4 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___lambda__1___closed__2;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@@ -7361,6 +7368,72 @@ lean_dec(x_2);
 return x_8;
 }
 }
+lean_object* _init_l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("NIY");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__1;
+x_2 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__2;
+x_2 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+lean_object* x_6; lean_object* x_7; 
+x_6 = l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__3;
+x_7 = l_Lean_throwError___at_Lean_PrettyPrinter_Formatter_formatterForKind___spec__1___rarg(x_6, x_1, x_2, x_3, x_4, x_5);
+return x_7;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___boxed), 5, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+lean_object* x_6; 
+x_6 = l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg(x_1, x_2, x_3, x_4, x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_6;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
 lean_object* l_Lean_PrettyPrinter_Formatter_unquotedSymbol_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
@@ -7787,6 +7860,7 @@ return x_13;
 lean_object* initialize_Init(lean_object*);
 lean_object* initialize_Lean_CoreM(lean_object*);
 lean_object* initialize_Lean_Parser_Extension(lean_object*);
+lean_object* initialize_Lean_Parser_StrInterpolation(lean_object*);
 lean_object* initialize_Lean_KeyedDeclsAttribute(lean_object*);
 lean_object* initialize_Lean_ParserCompiler_Attribute(lean_object*);
 lean_object* initialize_Lean_PrettyPrinter_Backtrack(lean_object*);
@@ -7804,6 +7878,9 @@ lean_dec_ref(res);
 res = initialize_Lean_Parser_Extension(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Lean_Parser_StrInterpolation(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 res = initialize_Lean_KeyedDeclsAttribute(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
@@ -7967,6 +8044,12 @@ l_Lean_PrettyPrinter_Formatter_quotedSymbol_formatter___closed__2 = _init_l_Lean
 lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_quotedSymbol_formatter___closed__2);
 l_Lean_PrettyPrinter_Formatter_quotedSymbol_formatter___closed__3 = _init_l_Lean_PrettyPrinter_Formatter_quotedSymbol_formatter___closed__3();
 lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_quotedSymbol_formatter___closed__3);
+l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__1 = _init_l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__1();
+lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__1);
+l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__2 = _init_l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__2();
+lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__2);
+l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__3 = _init_l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__3();
+lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___rarg___closed__3);
 l_Lean_PrettyPrinter_format___closed__1 = _init_l_Lean_PrettyPrinter_format___closed__1();
 lean_mark_persistent(l_Lean_PrettyPrinter_format___closed__1);
 l_Lean_PrettyPrinter_format___closed__2 = _init_l_Lean_PrettyPrinter_format___closed__2();

stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.PrettyPrinter.Parenthesizer
-// Imports: Init Lean.CoreM Lean.KeyedDeclsAttribute Lean.Parser.Extension Lean.ParserCompiler.Attribute Lean.PrettyPrinter.Backtrack
+// Imports: Init Lean.CoreM Lean.KeyedDeclsAttribute Lean.Parser.Extension Lean.Parser.StrInterpolation Lean.ParserCompiler.Attribute Lean.PrettyPrinter.Backtrack
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -55,6 +55,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkStackTop_parenthesizer___bo
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___rarg(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_identNoAntiquot_parenthesizer___boxed(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__8;
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkCategoryParenthesizerAttribute___lambda__1___closed__3;
 extern lean_object* l_Lean_Parser_regBuiltinCommandParserAttr___closed__4;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -64,6 +65,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(lean_object
 lean_object* l_Lean_PrettyPrinter_mkCategoryParenthesizerAttribute___closed__7;
 lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__10;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__3;
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__3;
 extern lean_object* l_Prod_HasRepr___rarg___closed__1;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_unicodeSymbol_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___lambda__1___closed__6;
@@ -216,6 +218,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_categoryParserOfStack_parenthesi
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_getConstInfo___rarg___lambda__1___closed__5;
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Unhygienic_MonadQuotation___closed__4;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_setExpected_parenthesizer___boxed(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___lambda__1___closed__3;
@@ -291,8 +294,10 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_visitToken___rarg___boxed(lean_o
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkNoWsBefore_parenthesizer___rarg(lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute(lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__1;
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkNoImmediateColon_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_nullKind___closed__2;
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__1;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_parenthesizeCategoryCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MonadTracer_trace___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_MonadTraverser_goRight___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__8___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -329,6 +334,7 @@ uint8_t l_Lean_Parser_isParserCategory(lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_combinatorParenthesizerAttribute;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___lambda__2(lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__2;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_notFollowedByCategoryToken_parenthesizer___rarg(lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__8;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkStackTop_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -385,6 +391,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_mkAntiquot_parenthesizer_x27___b
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_optional_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkColGt_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_MonadTraverser_getIdx___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__1___boxed(lean_object*);
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkCategoryParenthesizerAttribute___closed__2;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_lookahead_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkCombinatorParenthesizerAttribute(lean_object*);
@@ -3817,7 +3824,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__8;
-x_2 = lean_unsigned_to_nat(210u);
+x_2 = lean_unsigned_to_nat(211u);
 x_3 = lean_unsigned_to_nat(4u);
 x_4 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__9;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@@ -9119,6 +9126,72 @@ lean_dec(x_1);
 return x_2;
 }
 }
+lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("NIY");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__1;
+x_2 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__2;
+x_2 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; lean_object* x_5; 
+x_4 = l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__3;
+x_5 = l_Lean_throwError___at_Lean_PrettyPrinter_Parenthesizer_throwError___spec__1___rarg(x_4, x_1, x_2, x_3);
+return x_5;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___boxed), 3, 0);
+return x_4;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg(x_1, x_2, x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_4;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer(x_1, x_2, x_3);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_4;
+}
+}
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_ite___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
 _start:
 {
@@ -9453,6 +9526,7 @@ lean_object* initialize_Init(lean_object*);
 lean_object* initialize_Lean_CoreM(lean_object*);
 lean_object* initialize_Lean_KeyedDeclsAttribute(lean_object*);
 lean_object* initialize_Lean_Parser_Extension(lean_object*);
+lean_object* initialize_Lean_Parser_StrInterpolation(lean_object*);
 lean_object* initialize_Lean_ParserCompiler_Attribute(lean_object*);
 lean_object* initialize_Lean_PrettyPrinter_Backtrack(lean_object*);
 static bool _G_initialized = false;
@@ -9472,6 +9546,9 @@ lean_dec_ref(res);
 res = initialize_Lean_Parser_Extension(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Lean_Parser_StrInterpolation(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 res = initialize_Lean_ParserCompiler_Attribute(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
@@ -9724,6 +9801,12 @@ l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__1 = _init_l_Lean
 lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__1);
 l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__2 = _init_l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__2();
 lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__2);
+l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__1 = _init_l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__1();
+lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__1);
+l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__2 = _init_l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__2();
+lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__2);
+l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__3 = _init_l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__3();
+lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___rarg___closed__3);
 l_Lean_PrettyPrinter_parenthesize___closed__1 = _init_l_Lean_PrettyPrinter_parenthesize___closed__1();
 lean_mark_persistent(l_Lean_PrettyPrinter_parenthesize___closed__1);
 l_Lean_PrettyPrinter_parenthesize___closed__2 = _init_l_Lean_PrettyPrinter_parenthesize___closed__2();