max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/grind
History
Joachim Breitner e575736cae
feat: fun_induction to unfold function application in the goal (#8104) 
This PR makes `fun_induction` and `fun_cases` (try to) unfold the
function application of interest in the goal. The old behavior can be
enabled with `set_option tactic.fun_induction.unfolding false`. For
`fun_cases` this does not work yet when the function’s result type
depends on one of the arguments, see issue #8296.
2025-05-13 09:37:39 +00:00
..
experiments feat: add @[grind] annotations for HashMap (#8246) 2025-05-13 04:56:41 +00:00
grind_congrArg.lean chore: add failing grind tests (#8289) 2025-05-12 06:33:38 +00:00
grind_ite_funinduction.lean feat: fun_induction to unfold function application in the goal (#8104) 2025-05-13 09:37:39 +00:00
hashmap_getKey_eq.lean chore: failing test for grind (#8065) 2025-04-28 10:46:19 +00:00
palindrome.lean chore: add failing grind test (#8288) 2025-05-12 06:10:25 +00:00
qsort_ematch_local_theorem.lean chore: add failing grind tests (#8289) 2025-05-12 06:33:38 +00:00
README.md

README.md

Aspirational test cases for grind

These are not expected to work yet; we're collecting examples that we'd like to make work!