Instances are always exposed

Open Beginner friendly
#935 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
2/5
Estimated time
1-3 hours
Newbie friendliness
68/100
Issue type
Documentation
Clarity
Mostly clear
Activity status
Active
Domain
documentation

Research direction

Start by locating the reference-manual section that explains instances and review how automatic exposure is described. Update the manual so this behavior is easy to find and unambiguous, then verify the resulting documentation builds successfully.

Written by the indexing model from the issue text.

Description

doc-request

What question should the reference manual answer?

It is currently impossible to find in the manual that instances are always automatically exposed, if I'm not mistaken.

Dominant language
Lean
Stars
129
Forks
67
Avg merge
1d 15h
Merged PRs (30d)
16

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from leanprover/reference-manual

All issues in leanprover/reference-manual

Similar issues

More Documentation issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.