[ ] Maximum for automatic church numerals (large numbers can overflow the stack)
[ ] Maximum steps for beta-reduction
[ ] Predefined definitions (with a warning if you shadow it)
[ ] Option to disable syntax sugar such as automatic church numerals, definitions, etc.
[ ] Spans that point to different files (so that the embedder can surround the user code with an application to pass in data–errors should point to a different "file" in that case)