lean4-htt/src
Leonardo de Moura a435f3d641 feat: reduce s.1 =?= v to s =?= ⟨v⟩ if structure has a single field
This feature was suggested by @dselsam at PR #521.
It closes #509
2021-06-11 11:23:19 -07:00
..
bin chore: restore LEANC_EXTRA_FLAGS 2021-06-06 15:34:44 +02:00
cmake
include/lean chore: add Hashable that uses UInt64 2021-06-02 07:47:41 -07:00
Init chore: parameter naming convention 2021-06-06 17:09:26 -07:00
initialize
kernel chore: remove HashableUSize 2021-06-02 09:58:46 -07:00
Lean feat: reduce s.1 =?= v to s =?= ⟨v⟩ if structure has a single field 2021-06-11 11:23:19 -07:00
Leanpkg fix: leanpkg: rebuild if dependencies or leanpkg.toml (e.g. lean_version) changed 2021-05-30 17:29:54 +02:00
library feat: complain more verbosely 2021-06-06 15:34:44 +02:00
runtime fix: change IO.FS.Handle.read to return empty array at EOF 2021-06-08 13:17:53 +02:00
shared
shell chore: use leanc for all C code 2021-06-06 15:34:44 +02:00
Std chore: remove HashableUSize 2021-06-02 09:58:46 -07:00
tests/util
util chore: remove workaround 2021-06-02 08:06:52 -07:00
CMakeLists.txt chore: revert Windows workaround 2021-06-07 18:14:21 +02:00
config.h.in feat: version information API 2020-12-29 14:42:48 -08:00
githash.h.in
Init.lean fix: Not should not be reducible, special support for Ne 2021-02-15 17:36:11 -08:00
Lean.lean feat: environment extension for storing declaration ranges 2021-01-10 18:25:56 -08:00
lean.mk.in feat: Lean.js can compile itself 2021-06-06 15:34:44 +02:00
Leanpkg.lean fix: leanpkg: make flags; extend test 2021-05-30 17:29:54 +02:00
Std.lean chore: move nondet to Std/Control/Nondet.lean 2021-03-02 07:57:25 -08:00
stdlib.make.in chore: use leanc for all C code 2021-06-06 15:34:44 +02:00
version.h.in feat: version information API 2020-12-29 14:42:48 -08:00