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

chore: improve "no elaborator" error message

Browse source
This commit is contained in:
Sebastian Ullrich 2021-02-17 11:52:22 +01:00
parent 1a7535263e
commit 010338cb18
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/Term.lean
View file

@ -909,7 +909,7 @@ private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catch
let k := stx.getKind
match table.find? k with
| some elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
| none => throwError! "elaboration function for '{k}' has not been implemented"
| none => throwError! "elaboration function for '{k}' has not been implemented{indentD stx}"
instance : MonadMacroAdapter TermElabM where
getCurrMacroScope := getCurrMacroScope