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

chore(kernel/expr): remove leftover

Browse source
This commit is contained in:
Leonardo de Moura 2018-11-09 11:55:02 -08:00
parent 37df96e3e7
commit 9e7d1d5bd2
1 changed files with 0 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/expr.h
View file

@ -87,9 +87,6 @@ inductive expr
| lit : literal → expr
| mdata : kvmap → expr → expr
| proj : name → nat → expr → expr
-- The following constructor will be deleted
| quote : bool → expr → expr
*/
enum class expr_kind { BVar, FVar, MVar, Sort, Const, App, Lambda, Pi, Let, Lit, MData, Proj };
class expr : public object_ref {
@ -108,7 +105,6 @@ class expr : public object_ref {
friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & b);
/* legacy constructors */
friend expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info bi);
friend expr mk_quote(bool reflected, expr const & val);
public:
expr();
expr(expr const & other):object_ref(other) {}