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

feat(kernel/type_checker): add ensure_type variant

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-11 17:32:17 -08:00
parent e897bbdeb9
commit 8b3e97d285
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/kernel/type_checker.h
View file

@ -185,6 +185,7 @@ public:
expr ensure_pi(expr const & e, constraint_seq & cs) { auto r = ensure_pi(e); cs += r.second; return r.first; }
expr ensure_pi(expr const & e, expr const & s, constraint_seq & cs) { auto r = ensure_pi(e, s); cs += r.second; return r.first; }
expr ensure_sort(expr const & t, expr const & s, constraint_seq & cs) { auto r = ensure_sort(t, s); cs += r.second; return r.first; }
expr ensure_type(expr const & e, constraint_seq & cs) { auto r = ensure_type(e); cs += r.second; return r.first; }
bool is_def_eq(expr const & t, expr const & s, justification const & j, constraint_seq & cs) {
auto r = is_def_eq(t, s, j);