Leonardo de Moura cabb4350d9 feat(library): instances are not reducible by default anymore ... Motivation: see "Other goodies" section at https://github.com/leanprover/lean/wiki/Refactoring-structures We had to add a new transparency mode: Instances at type_context. In this mode, instances and reducible definitions are considered transparent. The new mode is used in the defeq_canonizer, code generator, and sizeof lemma generation at inductive_compiler. We also use the new mode in the unfold tactics.		2017-04-26 14:10:11 -07:00
..
lean	feat(library): instances are not reducible by default anymore	2017-04-26 14:10:11 -07:00
.gitignore	chore(tests/lean,shell/lean): run leantests and leanruntests in parallel	2017-03-30 06:04:00 +02:00