Skip to content

doc: fix missing '$'#564

Merged
chenson2018 merged 1 commit into
leanprover:mainfrom
lengyijun:patch-1
May 12, 2026
Merged

doc: fix missing '$'#564
chenson2018 merged 1 commit into
leanprover:mainfrom
lengyijun:patch-1

Conversation

@lengyijun
Copy link
Copy Markdown
Contributor

@lengyijun lengyijun commented May 12, 2026

doc: fix missing '$'

@lengyijun lengyijun changed the title Update Defs.lean Doc: fix missing '$' May 12, 2026
@lengyijun lengyijun changed the title Doc: fix missing '$' doc: fix missing '$' May 12, 2026
@arademaker
Copy link
Copy Markdown
Collaborator

This is a minor edit, @chenson2018, can you approve?

Copy link
Copy Markdown
Collaborator

@chenson2018 chenson2018 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@chenson2018 chenson2018 added this pull request to the merge queue May 12, 2026
Merged via the queue into leanprover:main with commit 608cbe1 May 12, 2026
3 of 6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants