From 6e4b9f2cc10c0b85185b28f9ba2cf418e0b1b0df Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 7 Aug 2019 17:41:18 -0700
Subject: [PATCH] feat(library/init/lean/elaborator/command): elaborate
 `init_quot` command

---
 library/init/lean/elaborator/basic.lean   | 3 +++
 library/init/lean/elaborator/command.lean | 7 +++++++
 2 files changed, 10 insertions(+)

diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean
index aa48dbbb0d..26d0513c38 100644
--- a/library/init/lean/elaborator/basic.lean
+++ b/library/init/lean/elaborator/basic.lean
@@ -261,6 +261,9 @@ logError stx ("unknown declaration '" ++ toString declName ++ "'")
 def getEnv : Elab Environment :=
 do s ← get; pure s.env
 
+def setEnv (env : Environment) : Elab Unit :=
+modify $ fun s => { env := env, .. s }
+
 def elabTerm (stx : Syntax) : Elab Expr :=
 stx.ifNode
   (fun n => do
diff --git a/library/init/lean/elaborator/command.lean b/library/init/lean/elaborator/command.lean
index 949185cd09..756d5ec99c 100644
--- a/library/init/lean/elaborator/command.lean
+++ b/library/init/lean/elaborator/command.lean
@@ -179,6 +179,13 @@ fun n => do
   let idsStx := n.getArg 1;
   idsStx.mforArgs addUniverse
 
+@[builtinCommandElab «init_quot»] def elabInitQuot : CommandElab :=
+fun _ => do
+  env ← getEnv;
+  match env.addDecl Declaration.quotDecl with
+  | Except.ok env   => setEnv env
+  | Except.error ex => logElabException (ElabException.kernel ex)
+
 /- We just ignore Lean3 notation declaration commands. -/
 @[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()
 @[builtinCommandElab «reserve»] def elabReserve : CommandElab := fun _ => pure ()