From 83f5329aa355661566d91b3c8a64be71e350e3f9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 5 Oct 2020 19:13:15 -0700 Subject: [PATCH] chore: make missing case explicit --- src/Lean/Elab/Do.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index b8a657dd6c..62108003ec 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -786,7 +786,7 @@ partial def toTerm : Code → M Syntax | Code.reassign _ stx k => do k ← toTerm k; liftM $ reassignToTerm stx k | Code.action stx k => do k ← toTerm k; liftM $ actionToTerm stx k | Code.ite ref _ o c t e => do t ← toTerm t; e ← toTerm e; pure $ mkIte ref o c t e -| _ => liftM $ Macro.throwError Syntax.missing "WIP" +| Code.«match» _ _ _ _ => liftM $ Macro.throwError Syntax.missing "WIP" def run (code : Code) (m : Syntax) (uvars : Array Name := #[]) (kind := Kind.regular) : MacroM Syntax := do term ← toTerm code { m := m, kind := kind, uvars := uvars };