Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: fun_induction foo (no arguments) #7101

Merged
merged 23 commits into from
Feb 18, 2025
Merged

feat: fun_induction foo (no arguments) #7101

merged 23 commits into from
Feb 18, 2025

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Feb 16, 2025 •
edited
Loading

This PR implements fun_induction foo, which is like fun_induction foo x y z, only that it picks the arguments to use from a unique suitable call to foo in the goal.

nomeata added 16 commits February 13, 2025 12:43
@nomeata
Stash
f08c998
@nomeata
First PoC
2cf3447
@nomeata
structural recursion, implicit targets
db10283
@nomeata
Refine error messages
d5f4405
@nomeata
Extract common code
45ed013
@nomeata
Prepare fun_cases
00ac0c0
@nomeata
Use getFunInductName everywhere
6874e3e
@nomeata
feat: try? to use fun_induction
4656412 
This PR makes `try?` use `fun_induction` instead of `induction`.

Builds on top of #7069
@nomeata
Do less changs
042b11b
@nomeata
Merge branch 'joachim/funind-tactic' into joachim/funind-tactic-try
84de179
@nomeata
More very nice grind output
0220bc5
@nomeata
Tactic docstrings
01fd351
@nomeata
Merge branch 'master' of https://github.com/leanprover/lean4 into joa…
f373cdc 
…chim/funind-tactic
@nomeata
Merge branch 'joachim/funind-tactic' into joachim/funind-tactic-try
6471ee3
@nomeata
feat: fun_induction foo (no arguments)
cc991ed 
this PR implements `fun_induction foo`, which is like
`fun_induction foo x y z`, only that it picks the arguments to use from
a unique suitable call to `foo` in the goal.
@nomeata
Update test
f42f071
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 16, 2025 18:14 Inactive
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 16, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 16, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 96c6f9dc96218ac06d14965dd81d2cc8a7752e3b --onto ae9d12aeaa075578c7ee3a5a585d0f9fb89cedd2. (2025-02-16 18:29:46)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6f5bb3e8963bc85e8b3f0a1cd62d53a0ec4c498b --onto ae9d12aeaa075578c7ee3a5a585d0f9fb89cedd2. (2025-02-16 21:41:59)
  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-02-18 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2025-02-18 11:20:34)

@nomeata nomeata changed the base branch from joachim/funind-tactic-try to master February 16, 2025 21:03
@nomeata nomeata force-pushed the joachim/funind-ident branch from c2456c1 to 06f9cc9 Compare February 16, 2025 21:06
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 16, 2025 21:34 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 18, 2025 11:03 Inactive
@nomeata nomeata marked this pull request as ready for review February 18, 2025 12:16
@nomeata nomeata enabled auto-merge February 18, 2025 12:16
@nomeata nomeata added the changelog-language Language features, tactics, and metaprograms label Feb 18, 2025
@nomeata nomeata added this pull request to the merge queue Feb 18, 2025
Merged via the queue into master with commit a3b76aa Feb 18, 2025
19 of 21 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@nomeata @leanprover-community-bot