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

fix: if-then-else is not builtin notation

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-24 07:54:20 -08:00
parent 0e2e2fc3f6
commit 79c15de131
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/Quotation.lean
View file

@ -254,7 +254,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
covered (adaptRhs rhsFn ∘ noOpMatchAdaptPats taken) (exhaustive := sz.isNone)
else uncovered
| _ => uncovered,
doMatch := fun yes no => do `(if Syntax.isOfKind discr $(quote k) then $(← yes []) else $(← no)),
doMatch := fun yes no => do `(cond (Syntax.isOfKind discr $(quote k)) $(← yes []) $(← no)),
}
else throwErrorAt! anti "match_syntax: antiquotation must be variable {anti}"
else if isAntiquotSuffixSplice quoted then throwErrorAt quoted "unexpected antiquotation splice"