Skip to content

feat: fun_induction foo (no arguments)#7101

Merged
nomeata merged 23 commits intomasterfrom
joachim/funind-ident
Feb 18, 2025
Merged

feat: fun_induction foo (no arguments)#7101
nomeata merged 23 commits intomasterfrom
joachim/funind-ident

Conversation

@nomeata
Copy link
Copy Markdown
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
@ghost
Copy link
Copy Markdown

ghost commented Feb 16, 2025 •
edited by ghost
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 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
17 of 19 checks passed
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 24, 2025
@nomeata @luisacicolini
feat: fun_induction foo (no arguments) (leanprover#7101)
4f86676 
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.
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 25, 2025
@nomeata @luisacicolini
feat: fun_induction foo (no arguments) (leanprover#7101)
eef4537 
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.
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 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.

1 participant

@nomeata