Right now, this is only an elaborator; there is no notion of top-level declaration, and no parser.