7 commits

Author	SHA1	Message	Date
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)