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
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