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

fix(frontends/lean/old_elaborator): remove "old" [intro]

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-10 10:39:34 -07:00
parent df113de725
commit f79e46a8a0
1 changed files with 0 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/old_attributes.cpp
View file

@ -37,14 +37,6 @@ void initialize_old_attributes() {
[](environment const & env, name const & n) {
return LEAN_DEFAULT_PRIORITY;
});
register_prio_attribute("intro", "introduction rule for backward chaining",
[](environment const & env, io_state const & ios, name const & d, unsigned prio, name const & ns, bool persistent) {
return env;
},
[](environment const &, name const &) { return false; },
[](environment const & env, name const & d) {
return LEAN_DEFAULT_PRIORITY;
});
}
void finalize_old_attributes() {}
}