Document `strong_coinduct`
Nobody has claimed this yet.
Assessment
- Difficulty
- 2/5
- Estimated time
- 1-3 hours
- Newbie friendliness
- 78/100
- Issue type
- Documentation
- Clarity
- Clearly specified
- Activity status
- Active
- Domain
- documentation
Research direction
Start with the reference manual section covering coinductive definitions and use the issue's infSeq example and #check output as the documentation requirements. Document strong_coinduct, including its hypothesis and applicability to mutually recursive and mixed inductive-coinductive definitions; done when these cases are clearly explained with the relevant example.
Written by the indexing model from the issue text.
Description
In lean4#14855 a support for strong coinduction was added. For example:
coinductive infSeq {r : α → α → Prop} : α → Prop where
| mk : r a b → infSeq b → infSeq a
/--
info: infSeq.coinduct.{u_1} {α : Sort u_1} {r : α → α → Prop} (pred : α → Prop)
(hyp : ∀ (a : α), pred a → ∃ b, r a b ∧ pred b) (a✝ : α) : pred a✝ → infSeq a✝
-/
#guard_msgs in
#check infSeq.coinduct
/--
info: infSeq.strong_coinduct.{u_1} {α : Sort u_1} {r : α → α → Prop} (pred : α → Prop)
(hyp : ∀ (a : α), pred a → ∃ b, r a b ∧ (pred b ∨ infSeq b)) (a✝ : α) : pred a✝ → infSeq a✝
-/
#guard_msgs in
#check infSeq.strong_coinduct
Note, that this also works for mutually-recursive (including mixed inductive-coinductive) definitions.
- Dominant language
- Lean
- Stars
- 129
- Forks
- 67
- Avg merge
- 1d 15h
- Merged PRs (30d)
- 16
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/reference-manual
-
doc-request
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
leanprover/reference-manual#936 ·
-
doc-request
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
leanprover/reference-manual#935 ·
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/reference-manual#896 ·
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/reference-manual#890 ·
-
doc-request
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/reference-manual#884 ·
All issues in leanprover/reference-manual
Similar issues
-
user-reported
Difficulty 2/5 1-3 hours Newbie friendliness 85/100
Kong/developer.konghq.com#7316 ·
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
HarperFast/skills#96 ·
-
Difficulty 2/5 1-3 hours Newbie friendliness 82/100
infinispan/infinispan#18150 ·
-
bug triage:deciding
Difficulty 1/5 Under an hour Newbie friendliness 88/100
open-telemetry/otel-arrow#4132 ·
-
Ecosystem: ClawMetry — the Qwen Code reader is now free and open source (follow-up to #9294 / #9338) Opencategory/integration priority/P3 scope/documentation status/ready-for-human type/feature-request
Difficulty 1/5 Under an hour Newbie friendliness 84/100