michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/type_context): make expand_macro public

Browse source
This commit is contained in:
Daniel Selsam 2015-11-04 17:45:54 -08:00 committed by Leonardo de Moura
parent f84f024b92
commit a104b478f3
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/type_context.h
View file

@ -147,7 +147,6 @@ class type_context {
bool m_check_types; bool m_check_types;
bool is_opaque(declaration const & d) const; bool is_opaque(declaration const & d) const;
optional<expr> expand_macro(expr const & m);
optional<expr> reduce_projection(expr const & e); optional<expr> reduce_projection(expr const & e);
optional<expr> norm_ext(expr const & e); optional<expr> norm_ext(expr const & e);
expr whnf_core(expr const & e); expr whnf_core(expr const & e);
@ -378,6 +377,9 @@ public:
bool has_assigned_uvar(levels const & ls) const; bool has_assigned_uvar(levels const & ls) const;
bool has_assigned_uvar_mvar(expr const & e) const; bool has_assigned_uvar_mvar(expr const & e) const;
/** \brief Expand macro using extension context */
optional<expr> expand_macro(expr const & m);
/** \brief Instantiate assigned universe unification variables occurring in \c l */ /** \brief Instantiate assigned universe unification variables occurring in \c l */
level instantiate_uvars(level const & l); level instantiate_uvars(level const & l);