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

feat(library/init/meta/expr): remove more occurrences of local_const

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-20 17:39:05 -07:00
parent 92ff42776c
commit e99036251c
1 changed files with 0 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/init/meta/expr.lean
View file

@ -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