Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / leanprover/reference-manual issues and pull requests

#46 - feat: add banner to prepare public release

Pull Request - State: closed - Opened by david-christiansen 4 months ago

#46 - feat: add banner to prepare public release

Pull Request - State: closed - Opened by david-christiansen 4 months ago

#45 - Basics of types and functions

Pull Request - State: closed - Opened by david-christiansen 4 months ago - 2 comments

#45 - Basics of types and functions

Pull Request - State: closed - Opened by david-christiansen 4 months ago - 2 comments

#44 - feat: support for draft mode

Pull Request - State: closed - Opened by david-christiansen 4 months ago

#44 - feat: support for draft mode

Pull Request - State: closed - Opened by david-christiansen 4 months ago

#43 - chore: update cache action version

Pull Request - State: closed - Opened by david-christiansen 4 months ago - 1 comment

#42 - feat: adapt to upstream linkifier feature

Pull Request - State: closed - Opened by david-christiansen 4 months ago

#42 - feat: adapt to upstream linkifier feature

Pull Request - State: closed - Opened by david-christiansen 4 months ago

#41 - feat: first draft of elaboration overview

Pull Request - State: closed - Opened by david-christiansen 4 months ago

#41 - feat: first draft of elaboration overview

Pull Request - State: closed - Opened by david-christiansen 4 months ago

#40 - chore: dependency and Lean update

Pull Request - State: closed - Opened by david-christiansen 4 months ago

#40 - chore: dependency and Lean update

Pull Request - State: closed - Opened by david-christiansen 4 months ago

#39 - feat: introduction

Pull Request - State: closed - Opened by david-christiansen 4 months ago

#37 - fix: incorporate tactic feedback

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#37 - fix: incorporate tactic feedback

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#36 - feat: start simp chapter

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#36 - feat: start simp chapter

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#35 - chore: word count reports in CI

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#35 - chore: word count reports in CI

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#34 - feat: begin tactics chapter

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#34 - feat: begin tactics chapter

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#33 - Branding update

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#33 - Branding update

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#32 - chore: resolve most TODOs in inductive types section

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#32 - chore: resolve most TODOs in inductive types section

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#30 - feat: Sidenotes

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#29 - feat: major improvements to cross-referencing

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#29 - feat: major improvements to cross-referencing

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#28 - role expander for `name` is not using scopes

Issue - State: closed - Opened by lecopivo 5 months ago - 1 comment

#28 - role expander for `name` is not using scopes

Issue - State: closed - Opened by lecopivo 5 months ago - 1 comment

#27 - fix: preserve scopes between Lean blocks

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#27 - fix: preserve scopes between Lean blocks

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#26 - chore: Lean and deps bump

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#26 - chore: Lean and deps bump

Pull Request - State: closed - Opened by david-christiansen 5 months ago

#25 - Inductive types

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#25 - Inductive types

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#24 - chore: bump to newest Verso

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#24 - chore: bump to newest Verso

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#23 - Document module syntax

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#23 - Document module syntax

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#22 - Links in inline ToCs go to the wrong page

Issue - State: closed - Opened by david-christiansen 6 months ago
Labels: bug

#22 - Links in inline ToCs go to the wrong page

Issue - State: closed - Opened by david-christiansen 6 months ago
Labels: bug

#21 - Small fixes

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#21 - Small fixes

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#20 - fix: branch name for Netlify deployment

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#20 - fix: branch name for Netlify deployment

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#19 - chore: bump Lean and Verso

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#19 - chore: bump Lean and Verso

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#18 - feat: Basics of Nat chapter

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#18 - feat: Basics of Nat chapter

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#17 - Improve section nesting and ToC display

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#17 - Improve section nesting and ToC display

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#16 - chore: option typo

Pull Request - State: closed - Opened by Kha 6 months ago - 1 comment

#16 - chore: option typo

Pull Request - State: closed - Opened by Kha 6 months ago - 1 comment

#15 - API reference should have source links?

Issue - State: open - Opened by kim-em 7 months ago - 1 comment
Labels: enhancement

#15 - API reference should have source links?

Issue - State: open - Opened by kim-em 7 months ago - 1 comment
Labels: enhancement

#14 - Hovering on `String.append : String → String → String` highlights two out of three `String`

Issue - State: open - Opened by kim-em 7 months ago - 2 comments
Labels: upstream-bug

#14 - Hovering on `String.append : String → String → String` highlights two out of three `String`

Issue - State: open - Opened by kim-em 7 months ago - 2 comments
Labels: upstream-bug

#13 - String interpolation example

Issue - State: open - Opened by kim-em 7 months ago - 1 comment

#12 - Lean has *three* kinds of string literals

Issue - State: closed - Opened by kim-em 7 months ago

#12 - Lean has *three* kinds of string literals

Issue - State: closed - Opened by kim-em 7 months ago

#11 - "This" could refer up or down

Issue - State: closed - Opened by kim-em 7 months ago

#9 - Clicking on subsections in the TOC goes to the section

Issue - State: closed - Opened by kim-em 7 months ago

#8 - feat: tools for documenting syntax

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#7 - fix: message duplication in log

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#6 - chore: try removing some TeX deps from CI

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#5 - doc: improve universe chapter

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#4 - doc: more text about Strings

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#3 - fix: improve line breaking in ToC CSS

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#2 - chore: add deployment target to README

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#1 - chore: get CI up and going

Pull Request - State: closed - Opened by david-christiansen 7 months ago