leanprover-community / leanprover-community/lean4-metaprogramming-book
The `Subset` example in the Syntax chapter is outdated
Open
Beginner friendly
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 310
- Forks
- 78
- Avg merge
- 2h 7m
- Merged PRs (30d)
- 4
Description
I am using Lean 4.25.2. The Syntax chapter contains:
instance : Subset (Set α) where
subset X Y := ∀ (x : α), x ∈ X → x ∈ Y
The class Subset seems to have been renamed to HasSubset, and subset to Subset. The following works with the current stable Lean version:
instance : HasSubset (Set α) where
Subset X Y := ∀ (x : α), x ∈ X → x ∈ Y
Contributor guide
No contributing guide indexed for this repository
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.
Research direction
Start with the Syntax chapter and locate the outdated Subset example shown in the issue. Update the example to use the current HasSubset and Subset names, then verify that the chapter no longer presents the obsolete form.
Written by the indexing model from the issue text.
Assessment
- Domain
- documentation
- Issue type
- Documentation
- Difficulty
- 1/5
- Estimated time
- Under an hour
- Activity status
- Stale
- Clarity
- Clearly specified
- Newbie friendliness
- 68/100