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

chore: style

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-18 18:27:52 -08:00
parent ad72ec4d0d
commit 1c6d6cccb9
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/Init/Lean/Elab/SynthesizeSyntheticMVars.lean
View file

@ -15,7 +15,7 @@ namespace Term
private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSorry := true) : TermElabM Expr :=
-- Remark: if `ctx.errToSorry` is already false, then we don't enable it. Recall tactics disable `errToSorry`
adaptReader (fun (ctx : Context) => { errToSorry := ctx.errToSorry && errToSorry, .. ctx }) $
elabTerm stx expectedType? false
elabTerm stx expectedType? false
/--
Try to elaborate `stx` that was postponed by an elaboration method using `Expection.postpone`.