Leonardo de Moura
de64750621
chore(frontends/lean): disable expressions that use tactic framework
2016-04-25 15:07:26 -07:00
Leonardo de Moura
9d0dfb8404
refactor(frontends/lean): remove calc_proof_elaborator
2016-03-03 17:22:45 -08:00
Jeremy Avigad
4050892889
refactor(library/*): rename 'compose' to 'comp'
2016-03-02 22:48:05 -05:00
Leonardo de Moura
f177082c3b
refactor(*): normalize metaclass names
...
@avigad and @fpvandoorn, I changed the metaclasses names. They
were not uniform:
- The plural was used in some cases (e.g., [coercions]).
- In other cases a cryptic name was used (e.g., [brs]).
Now, I tried to use the attribute name as the metaclass name whenever
possible. For example, we write
definition foo [coercion] ...
definition bla [forward] ...
and
open [coercion] nat
open [forward] nat
It is easier to remember and is uniform.
2015-12-28 10:39:15 -08:00
Jeremy Avigad
8ccafc4267
fix(library/init/function): fix typo
2015-12-22 16:39:13 -05:00
Leonardo de Moura
5a98a2538c
refactor(library): move basic simp/congr rules to init folder, delete some legacy files
2015-11-20 16:38:10 -08:00
Leonardo de Moura
744d1cba3d
feat(library,hott,frontends/lean): avoid keywords with hyphen
2015-11-08 14:04:54 -08:00
Leonardo de Moura
ede23a3267
feat(hott,library): add additional spacing hints
2015-09-30 17:41:44 -07:00
Leonardo de Moura
4b1b3e277f
feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]'
...
see issue #693
2015-07-07 16:37:06 -07:00
Leonardo de Moura
9f7c4aac69
feat(library): add helper lemmas for equivalent types
2015-07-06 12:17:57 -07:00
Leonardo de Moura
77d5657813
refactor(library/algebra/function): move function.lean to init folder
...
Motivation: this file defines basic things such as function composition.
In the HoTT library, it is located in the init folder.
2015-07-06 07:29:56 -07:00
