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

feat: avoid bizarre error message for definition without body

Browse source 
@kha This is a temporary hack to avoid a incomprehensible error
message. I will try to tweak the parser error recovery in another
commit.
This commit is contained in:
Leonardo de Moura 2021-03-31 14:53:24 -07:00
parent ae4f3242d4
commit c35f96ac82
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/MutualDef.lean
View file

@ -162,8 +162,10 @@ private def declValToTerm (declVal : Syntax) : MacroM Syntax := withRef declVal
expandMatchAltsWhereDecls declVal[0]
else if declVal.isOfKind `Lean.Parser.Term.whereDecls then
expandWhereDeclsAsStructInst declVal
else if declVal.isMissing then
Macro.throwErrorAt declVal "declaration body is missing"
else
Macro.throwErrorAt declVal "unexpected definition value"
Macro.throwErrorAt declVal "unexpected declaration body"
private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array Expr) :=
headers.mapM fun header => withDeclName header.declName $ withLevelNames header.levelNames do

2
src/Lean/Parser/Command.lean
View file

@ -34,7 +34,7 @@ def declSig := leading_parser many (ppSpace >> (Term.simpleBinderWithou
def optDeclSig := leading_parser many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.optType
def declValSimple := leading_parser " :=\n" >> termParser >> optional Term.whereDecls
def declValEqns := leading_parser Term.matchAltsWhereDecls
def declVal := declValSimple <|> declValEqns <|> Term.whereDecls
def declVal := declValSimple <|> declValEqns <|> Term.whereDecls <|> error "unexpected declaration body"
def «abbrev» := leading_parser "abbrev " >> declId >> optDeclSig >> declVal
def «def» := leading_parser "def " >> declId >> optDeclSig >> declVal
def «theorem» := leading_parser "theorem " >> declId >> declSig >> declVal