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

feat(frontends/lean/builtin_cmds): print metas for patterns

Browse source
This commit is contained in:
Daniel Selsam 2015-12-07 11:42:34 -08:00 committed by Leonardo de Moura
parent af7ffcf575
commit a9aeb69789
1 changed files with 12 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/frontends/lean/builtin_cmds.cpp
View file

@ -237,10 +237,20 @@ static void print_patterns(parser & p, name const & n) {
if (is_forward_lemma(p.env(), n)) {
// we regenerate the patterns to make sure they reflect the current set of reducible constants
try {
if (auto mps = mk_multipatterns(p.env(), p.ios(), n)) {
blast::scope_debug scope(p.env(), p.ios());
auto hi = blast::mk_hi_lemma(n, LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY);
if (hi.m_multi_patterns) {
io_state_stream out = p.regular_stream();
out << "(multi-)patterns:\n";
for (multi_pattern const & mp : mps) {
if (!is_nil(hi.m_mvars)) {
expr m = head(hi.m_mvars);
out << m << " : " << mlocal_type(m);
for (expr const & m : tail(hi.m_mvars)) {
out << ", " << m << " : " << mlocal_type(m);
}
}
out << "\n";
for (multi_pattern const & mp : hi.m_multi_patterns) {
out << "{";
bool first = true;
for (expr const & p : mp) {