| .. |
|
control
|
chore(library/init/control/except): missing @[inline] annotations
|
2018-09-19 09:13:49 -07:00 |
|
data
|
chore(library/init/data/ordering/basic): mark cmp_using as [inline]
|
2018-09-17 14:56:31 -07:00 |
|
lean
|
feat(library/init/lean/parser/term): lambda, pi, arrow
|
2018-09-19 12:36:34 -07:00 |
|
meta
|
refactor(library/init/core): change ite signature
|
2018-09-17 14:27:28 -07:00 |
|
coe.lean
|
fix(library/init): missing @[inline]
|
2018-09-18 21:42:22 -07:00 |
|
core.lean
|
feat(library/init/core): use cases_on instead of rec_on
|
2018-09-18 15:25:15 -07:00 |
|
default.lean
|
chore(library/init/meta): remove well_founded_tactics
|
2018-08-23 15:14:22 -07:00 |
|
env_ext.lean
|
chore(library/init/env_ext): update
|
2018-09-11 13:55:25 -07:00 |
|
function.lean
|
chore(library/init): avoid calc at corelib
|
2018-08-27 12:17:30 -07:00 |
|
init.md
|
chore(*.md): fix/remove broken links
|
2016-02-23 10:11:24 -08:00 |
|
io.lean
|
chore(library): remove >>, we should use *>
|
2018-09-12 17:31:21 -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 |
