lean4-htt/src
Joachim Breitner 18c97926a1
refactor: extract withRecArgInfo from findRecArg (#4549)
this is  in preparation for #4542, and extracts from `findRecArg` the
functionality for trying one particular argument.

It also refactors the code a bit. In particular

 * It reports errors in the order of the parameters, not the order of
   in which they are tried (it tries non-indices first).
 * For every argument it will say why it wasn't tried, even if the
   reason is quite obviously (fixed prefix, or `Prop`-typed etc.)

Therefore there is some error message churn.
2024-06-26 11:10:57 +00:00
..
bin
cmake
include/lean fix: validate UTF-8 at C++ -> Lean boundary (#3963) 2024-06-19 14:05:48 +00:00
Init feat: maximum?_eq_some_iff' (#4550) 2024-06-24 11:57:27 +00:00
initialize
kernel feat: propagate maxHeartbeats to kernel (#4113) 2024-05-09 17:44:19 +00:00
lake fix: lake: non-ident script names (#4564) 2024-06-26 04:24:01 +00:00
Lean refactor: extract withRecArgInfo from findRecArg (#4549) 2024-06-26 11:10:57 +00:00
library refactor: port below and brecOn construction to Lean (#4517) 2024-06-26 11:10:39 +00:00
runtime fix: validate UTF-8 at C++ -> Lean boundary (#3963) 2024-06-19 14:05:48 +00:00
shell fix: do not dllexport symbols in core static libraries (#3601) 2024-03-15 11:58:34 +00:00
Std feat: introduce Std (#4499) 2024-06-21 07:08:45 +00:00
util feat: expose flags for the bundled C compiler (#4477) 2024-06-22 01:23:33 +00:00
CMakeLists.txt feat: introduce Std (#4499) 2024-06-21 07:08:45 +00:00
config.h.in
githash.h.in
Init.lean feat: grind normalization theorems (#4164) 2024-05-14 19:19:38 +00:00
lakefile.toml.in feat: introduce Std (#4499) 2024-06-21 07:08:45 +00:00
lean-toolchain
Lean.lean feat: propagate maxHeartbeats to kernel (#4113) 2024-05-09 17:44:19 +00:00
lean.mk.in fix: do not dllexport symbols in core static libraries (#3601) 2024-03-15 11:58:34 +00:00
Leanc.lean feat: expose flags for the bundled C compiler (#4477) 2024-06-22 01:23:33 +00:00
Std.lean feat: introduce Std (#4499) 2024-06-21 07:08:45 +00:00
stdlib.make.in feat: introduce Std (#4499) 2024-06-21 07:08:45 +00:00
stdlib_flags.h chore: unset parseQuotWithCurrentStage in stage1’s src/stdlib_flags.h (#4537) 2024-06-23 09:44:14 +00:00
version.h.in