From e99036251c8b1842c4afed920f0ac8a88faef3ce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 20 May 2018 17:39:05 -0700 Subject: [PATCH] feat(library/init/meta/expr): remove more occurrences of local_const --- library/init/meta/expr.lean | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index 17c43f7ae6..317887d503 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -383,16 +383,6 @@ meta def is_numeral : expr → bool meta def imp (a b : expr) : expr := pi `_ binder_info.default a b -meta def lambdas : list expr → expr → expr -| (local_const uniq pp info t :: es) f := - lam pp info t (abstract_local (lambdas es f) uniq) -| _ f := f - -meta def pis : list expr → expr → expr -| (local_const uniq pp info t :: es) f := - pi pp info t (abstract_local (pis es f) uniq) -| _ f := f - meta def extract_opt_auto_param : expr → expr | `(@opt_param %%t _) := extract_opt_auto_param t | `(@auto_param %%t _) := extract_opt_auto_param t