10 commits

Author	SHA1	Message	Date
Leonardo de Moura	320b2c9961	fix: use getConstNoEx for implementing smart unfolding	2019-11-11 11:30:22 -08:00
Leonardo de Moura	0358511121	chore: add helper	2019-11-11 11:30:22 -08:00
Leonardo de Moura	b771ec7328	feat: add basic HasToString Meta.Exception instance	2019-11-11 11:30:22 -08:00
Leonardo de Moura	269ae853b8	feat: add FunInfo	2019-11-10 18:26:57 -08:00
Leonardo de Moura	fd3786b585	chore: simplify FunInfo cache	2019-11-10 17:27:33 -08:00
Leonardo de Moura	25fed41446	feat: add forallBoundedTelescope	2019-11-10 17:12:13 -08:00
Leonardo de Moura	8653082133	fix: must take BinderInfo into account in the elaborator ... This is not needed in the `TacticM` monad. So, we should check if this is a bottleneck and the future.	2019-11-10 16:51:30 -08:00
Leonardo de Moura	82f521119c	feat: add isPropAux and caches for FunInfo module, rename byUnfoldingReducibleOnly => usingTransparency,	2019-11-10 16:49:07 -08:00
Leonardo de Moura	a21a024172	feat: add Meta/DefEq.lean	2019-11-10 08:55:26 -08:00
Leonardo de Moura	41fccd976b	refactor: add Lean.Meta directory for MetaM monad	2019-11-10 08:04:00 -08:00

Renamed from library/Init/Lean/Meta.lean (Browse further)