max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: make missing case explicit

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-05 19:13:15 -07:00
parent eac3ca9286
commit 83f5329aa3
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Do.lean
View file

@ -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 };