| .. |
|
meta
|
feat(library/init/meta/converter): implement conversionals using ext_simplify_core
|
2016-10-19 17:23:32 -07:00 |
|
.gdb_history
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
algebra.lean
|
feat(library/init): add order structures
|
2016-10-02 13:33:25 -07:00 |
|
alternative.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
applicative.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
binary.lean
|
feat(library/init/binary): add basic binary properties
|
2016-09-30 20:26:22 -07:00 |
|
bool.lean
|
chore(library/init/bool): add xor for Booleans
|
2016-10-07 14:21:11 -07:00 |
|
char.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
classical.lean
|
refactor(library/tactic/simplify): add simplify subclasses, and use new simplifier at nested
|
2016-10-18 16:18:25 -07:00 |
|
coe.lean
|
feat(library/init/coe,frontends/lean): more general coercions to fun
|
2016-09-27 15:41:06 -07:00 |
|
combinator.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
congr.lean
|
refactor(library/tactic/simplify): delete old simplifier
|
2016-10-19 14:03:14 -07:00 |
|
core.lean
|
refactor(library/init/core): define nat.add using equations
|
2016-10-11 14:10:49 -07:00 |
|
default.lean
|
refactor(library/tactic/simplify): delete old simplifier
|
2016-10-19 14:03:14 -07:00 |
|
fin.lean
|
chore(library/init): use 'instance'
|
2016-09-23 14:00:34 -07:00 |
|
function.lean
|
chore(library/init/function): cleanup
|
2016-10-07 14:09:52 -07:00 |
|
functor.lean
|
chore(library/init): definition => def
|
2016-10-06 16:04:12 -07:00 |
|
funext.lean
|
chore(library/init): definition => def
|
2016-10-06 16:04:12 -07:00 |
|
id_locked.lean
|
chore(frontends/lean): remove 'new_elaborator' option
|
2016-09-20 08:32:37 -07:00 |
|
init.md
|
chore(*.md): fix/remove broken links
|
2016-02-23 10:11:24 -08:00 |
|
instances.lean
|
feat(frontends/lean): anonymous instances
|
2016-09-23 13:34:34 -07:00 |
|
list.lean
|
fix(meta/mk_dec_eq_instance): handle indices and ginductives
|
2016-10-13 10:12:37 -07:00 |
|
list_classes.lean
|
refactor(library/init): reorganize files and cleanup notation
|
2016-09-25 13:37:45 -07:00 |
|
logic.lean
|
refactor(library/tactic/simplify): add simplify subclasses, and use new simplifier at nested
|
2016-10-18 16:18:25 -07:00 |
|
monad.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
monad_combinators.lean
|
refactor(library/init/bool): put main operations in the top-level
|
2016-09-25 13:32:15 -07:00 |
|
nat.lean
|
chore(library/init/core): use equations
|
2016-10-07 14:58:17 -07:00 |
|
nat_div.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
num.lean
|
refactor(library/init/bool): put main operations in the top-level
|
2016-09-25 13:32:15 -07:00 |
|
option.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
order.lean
|
feat(library/init): add order structures
|
2016-10-02 13:33:25 -07:00 |
|
ordering.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
prod.lean
|
feat(frontends/lean): anonymous instances
|
2016-09-23 13:34:34 -07:00 |
|
quot.lean
|
feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword
|
2016-09-24 18:40:57 -07:00 |
|
relation.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
set.lean
|
refactor(library/init): simplify has_emptyc type class
|
2016-09-27 10:03:57 -07:00 |
|
setoid.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
sigma.lean
|
chore(library/init): definition => def
|
2016-10-06 16:04:12 -07:00 |
|
sigma_lex.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
state.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
string.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
subtype.lean
|
refactor(library/init): reorganize files and cleanup notation
|
2016-09-25 13:37:45 -07:00 |
|
sum.lean
|
feat(frontends/lean): anonymous instances
|
2016-09-23 13:34:34 -07:00 |
|
timeit.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
to_string.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
trace.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
unit.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
unsigned.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
|
wf.lean
|
chore(library/init): cleanup
|
2016-09-24 16:38:39 -07:00 |
