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

chore(library/metavar_context): add TODO's

Browse source
This commit is contained in:
Leonardo de Moura 2018-02-23 10:13:19 -08:00
parent 173eb1c6b7
commit 2cb018734e
2 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/metavar_context.cpp
View file

@ -53,10 +53,12 @@ static name mk_meta_decl_name() {
}
level metavar_context::mk_univ_metavar_decl() {
// TODO(Leo): use m_ngen.next() instead of mk_meta_decl_name
return mk_meta_univ(mk_meta_decl_name());
}
expr metavar_context::mk_metavar_decl(optional<name> const & pp_n, local_context const & ctx, expr const & type) {
// TODO(Leo): use m_ngen.next() instead of mk_meta_decl_name
name n = mk_meta_decl_name();
m_decls.insert(n, metavar_decl(ctx, head_beta_reduce(type)));
return mk_meta_ref(n, pp_n);

2
src/library/metavar_context.h
View file

@ -30,7 +30,7 @@ class metavar_context {
name_map<metavar_decl> m_decls;
name_map<level> m_uassignment;
name_map<expr> m_eassignment;
name_generator m_ngen;
name_generator m_ngen; // TODO(Leo): this field is not being used yet.
struct interface_impl;
friend struct interface_impl;