From 051fd530e0ee206166cf770b30dd3d1dfcb6de02 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Jan 2020 18:33:36 -0800 Subject: [PATCH] chore: handle new `let` at `toPreterm` --- src/Init/Lean/Elab/Quotation.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean index 68e5f2141b..59be25a69c 100644 --- a/src/Init/Lean/Elab/Quotation.lean +++ b/src/Init/Lean/Elab/Quotation.lean @@ -381,15 +381,16 @@ private unsafe partial def toPreterm : Syntax → TermElabM Expr e ← toPreterm stx; pure $ lctx.mkLambda #[mkFVar n] e | `Lean.Parser.Term.let => do - let ⟨n, val⟩ := show Name × Syntax from match (args.get! 1).getKind with - | `Lean.Parser.Term.letIdDecl => ((args.get! 1).getIdAt 0, (args.get! 1).getArg 4) - | `Lean.Parser.Term.letPatDecl => (((args.get! 1).getArg 0).getIdAt 0, (args.get! 1).getArg 3) - | _ => unreachable!; + let (n, val, body) := + if (args.get! 1).isIdent then + ((args.get! 1).getId, args.get! 5, args.get! 7) + else + ((args.get! 1).getIdAt 0, args.get! 4, args.get! 6); val ← toPreterm val; lctx ← getLCtx; let lctx := lctx.mkLetDecl n n exprPlaceholder val; adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $ do - e ← toPreterm $ args.get! 3; + e ← toPreterm $ body; pure $ lctx.mkLambda #[mkFVar n] e | `Lean.Parser.Term.let_core => -- parser! "let_core " >> termParser >> ":=" >> termParser >> "; " >> termParser