lean4-htt/src
Leonardo de Moura 2a0dc1804b feat: improve isRflProof and isRflTheorem
The `Eq.symm` of a `rfl` theorem is a `rfl` theorem, the application
of `rfl` theorem too.
2022-04-21 15:40:38 -07:00
..
bin chore: fix USE_GMP=OFF by removing GMP linking customization 2022-03-26 16:29:52 +01:00
cmake
include/lean fix: wait on tasks before Lean program exit 2021-12-15 15:58:24 +01:00
Init fix: simpAll and tests 2022-04-21 15:00:07 -07:00
initialize
kernel perf: efficient unsigned hash(expr const & e) 2022-03-15 07:15:00 -07:00
lake@d961d8cfaa chore: update Lake 2022-03-21 14:50:54 +01:00
Lean feat: improve isRflProof and isRflTheorem 2022-04-21 15:40:38 -07:00
library fix: debug build 2022-04-13 13:12:53 -07:00
runtime feat: add IO.monoNanosNow 2022-04-11 12:16:20 +02:00
shell chore: fix USE_GMP=OFF by removing GMP linking customization 2022-03-26 16:29:52 +01:00
Std chore: style 2022-04-07 17:35:05 -07:00
util chore: define WIN32_LEAN_AND_MEAN 2022-04-06 09:38:19 +02:00
CMakeLists.txt chore: define WIN32_LEAN_AND_MEAN 2022-04-06 09:38:19 +02:00
config.h.in
githash.h.in
Init.lean chore: link orphan file 2022-03-07 10:59:49 +01:00
Lean.lean feat: expose --load-dynlib functionality to Lean code 2021-12-15 08:26:48 +00:00
lean.mk.in feat: build .ilean files next to .olean files 2022-01-14 09:18:57 +01:00
Leanc.lean chore: fix USE_GMP=OFF by removing GMP linking customization 2022-03-26 16:29:52 +01:00
Std.lean
stdlib.make.in chore: fix USE_GMP=OFF by removing GMP linking customization 2022-03-26 16:29:52 +01:00
stdlib_flags.h Revert "chore: prefer native" 2021-10-26 20:19:27 +02:00
version.h.in