| .. |
|
control
|
fix(library/init/io): move coroutine_io implementation to io
|
2018-09-06 18:09:32 -07:00 |
|
data
|
chore(library/init/data/list/basic): remove unnecessary workaround
|
2018-09-07 17:10:23 -07:00 |
|
lean
|
feat(library/init/lean/{message,parser}): enhance lean.message
|
2018-09-08 18:37:58 -07:00 |
|
meta
|
feat(library/init/core): decidable_eq is a proper class
|
2018-09-07 16:38:11 -07:00 |
|
coe.lean
|
feat(library/init/core): decidable_eq is a proper class
|
2018-09-07 16:38:11 -07:00 |
|
core.lean
|
feat(library/init/core): decidable_eq is a proper class
|
2018-09-07 16:38:11 -07:00 |
|
default.lean
|
chore(library/init/meta): remove well_founded_tactics
|
2018-08-23 15:14:22 -07:00 |
|
env_ext.lean
|
doc(library/init/env_ext): document environment extensions in use
|
2018-05-30 14:28:49 -07:00 |
|
function.lean
|
chore(library/init): avoid calc at corelib
|
2018-08-27 12:17:30 -07:00 |
|
init.md
|
|
|
|
io.lean
|
fix(library/init/io): move coroutine_io implementation to io
|
2018-09-06 18:09:32 -07:00 |
|
platform.lean
|
feat(library/vm): add support for system.platform.nbits in the VM
|
2018-05-03 15:54:54 -07:00 |
|
util.lean
|
refactor(frontends/lean/elaborator): mark thunk as opaque, and thunk A to A is now a coercion
|
2018-08-21 15:27:51 -07:00 |
|
version.lean.in
|
chore(leanpkg/lean_version): recognize nightlies as releases separate from master
|
2018-03-20 15:14:45 -07:00 |
|
wf.lean
|
feat(kernel/inductive/inductive): dependent elimination for inductive predicates
|
2018-06-12 13:03:26 -07:00 |
