Commit graph

7 commits

Author SHA1 Message Date
Leonardo de Moura
8c11dc1ecd chore(library/data/quotient): rename aux.lean to util.lean (fix problem with cloning lean repository on Windows machine)
See
http://stackoverflow.com/questions/3689137/error-git-checkout-index-unable-to-create-file
for additional details
2014-09-11 14:57:15 -07:00
Leonardo de Moura
9412e604c8 refactor(library/data): cleanup datatypes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 22:31:52 -07:00
Leonardo de Moura
68d9bef860 refactor(library): add 'eq' and 'ne' namespaces
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 18:41:06 -07:00
Leonardo de Moura
364bba2129 feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 17:26:36 -07:00
Leonardo de Moura
8743394627 refactor(kernel/inductive): replace recursor name, use '.rec' instead of '_rec'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 15:04:57 -07:00
Leonardo de Moura
e51c4ad2e9 feat(frontends/lean): rename 'using' command to 'open'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 16:00:38 -07:00
Leonardo de Moura
dbaf81e16d refactor(library): remove unnecessary 'standard' subdirectory
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 18:08:09 -07:00
Renamed from library/standard/data/quotient/aux.lean (Browse further)