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 2019-12-22 07:25:27 -08:00
parent 7490c34b54
commit 80165d24a1
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/Term.lean
View file

@ -24,7 +24,7 @@ structure Context extends Meta.Context :=
(univNames : List Name := [])
(openDecls : List OpenDecl := [])
(macroStack : List Syntax := [])
(currMacroScope : MacroScope := 0)
(currMacroScope : MacroScope := 0)
/- When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`.
The function `elabTerm` catches this exception and creates fresh synthetic metavariable `?m`, stores `?m` in
the list of pending synthetic metavariables, and returns `?m`. -/