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

feat: display unsolved goals

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-16 20:25:22 -08:00
parent 8862a82aac
commit ccd7af0008
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Lean/Elab/Tactic.lean
View file

@ -33,8 +33,7 @@ withMVarContext mvarId $ fun ctx s =>
| EStateM.Result.ok a newS => EStateM.Result.ok a newS.toTermState
def reportUnsolvedGoals (ref : Syntax) (goals : List MVarId) : TermElabM Unit :=
-- TODO: pretty print goals
throwError ref "there are unsolved goals"
throwError ref $ "unsolved goals" ++ Format.line ++ MessageData.joinSep (goals.map $ MessageData.ofGoal) Format.line
def runTactic (ref : Syntax) (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
modify $ fun s => { mctx := s.mctx.instantiateMVarDeclMVars mvarId, .. s };