9 commits

Author	SHA1	Message	Date
Leonardo de Moura	b23e59d509	feat: allow #eval to update Environment ... See new `MetaHasEval`. cc @Kha	2020-07-30 16:48:31 -07:00
Leonardo de Moura	52353539c1	fix: track NameGenerator at CommandElabM ... @Kha This was a super nasty bug. We did not notice it before because most commands invoke `liftTermElabM` at most once. This is not true for the new `structure` command. The bug manifested itself while I was testing the new command. However, the issue was due to accidental reuse of fresh variable Ids :)	2020-07-27 14:31:43 -07:00
Leonardo de Moura	0118de09b9	chore: add mkAuxDefinition	2020-07-24 10:45:32 -07:00
Leonardo de Moura	232eefcef9	feat: add auxiliary constructions for inductive types	2020-07-15 16:32:23 -07:00
Leonardo de Moura	48c6c7c871	feat: report unused universe parameters	2020-07-14 16:40:56 -07:00
Leonardo de Moura	c8636f2bf7	chore: generalize withDeclId	2020-07-11 08:01:36 -07:00
Leonardo de Moura	249bda16c0	chore: remove prelude commands from Lean package	2020-06-25 11:21:17 -07:00
Sebastian Ullrich	52d966f70b	feat: #eval	2020-06-16 10:41:42 -07:00
Leonardo de Moura	4ccc3fef52	chore: move Init.Lean files to Lean package	2020-05-26 15:04:35 -07:00

Renamed from src/Init/Lean/Elab/Command.lean (Browse further)