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

feat(kernel/extension_context): add auxiliary method is_def_eq

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-27 11:17:54 -08:00
parent 928fc3ab81
commit 1dbe4b8fb7
2 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/extension_context.cpp
View file

@ -14,4 +14,7 @@ expr extension_context::whnf(expr const & e, constraint_seq & cs) {
expr extension_context::infer_type(expr const & e, constraint_seq & cs) { expr extension_context::infer_type(expr const & e, constraint_seq & cs) {
auto p = infer_type(e); cs += p.second; return p.first; auto p = infer_type(e); cs += p.second; return p.first;
} }
bool extension_context::is_def_eq(expr const & e1, expr const & e2, delayed_justification & j, constraint_seq & cs) {
auto p = is_def_eq(e1, e2, j); cs += p.second; return p.first;
}
} }

1
src/kernel/extension_context.h
View file

@ -31,5 +31,6 @@ public:
virtual name mk_fresh_name() = 0; virtual name mk_fresh_name() = 0;
expr whnf(expr const & e, constraint_seq & cs); expr whnf(expr const & e, constraint_seq & cs);
expr infer_type(expr const & e, constraint_seq & cs); expr infer_type(expr const & e, constraint_seq & cs);
bool is_def_eq(expr const & e1, expr const & e2, delayed_justification & j, constraint_seq & cs);
}; };
} }