From e5fec1ab00c208f8f73507a76df128c247cc9514 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 7 Dec 2018 10:32:09 +0100 Subject: [PATCH] feat(library/init/lean/elaborator): elaborate trivial headers --- library/init/lean/elaborator.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index 829da92789..5d66d2f57a 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -246,6 +246,13 @@ def declaration.elaborate : elaborator := pure () | _ := pure () +def module.header.elaborate : elaborator := +λ stx, do + let header := view module.header stx, + match header with + | {«prelude» := some _, imports := []} := pure () + | _ := error stx "not implemented: imports" + def prec_to_nat : option precedence.view → nat | (some prec) := prec.term.to_nat | none := 0 @@ -488,6 +495,7 @@ do ns ← view «namespace» <$> current_command, -- TODO(Sebastian): replace with attribute def elaborators : rbmap name coelaborator (<) := rbmap.from_list [ + (module.header.name, module.header.elaborate), (notation.name, notation.elaborate), (reserve_notation.name, reserve_notation.elaborate), (no_kind.name, no_kind.elaborate),