Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Copy binder types from actual declaration, fixes display of or.inl #151

Merged

Conversation

alexjbest
Copy link
Member

Currently doc-gen prints or.inl as

inductive or (a b : Prop) :
Prop
inl : ∀ (a b : Prop), a → a ∨ b
inr : ∀ (a b : Prop), b → a ∨ b

but #check or.inl gives or.inl : ∀ {a b : Prop}, a → a ∨ b with implicit a b.
To fix this we copy the binder types from the actual declaration to the local constants used to pretty print the type

@alexjbest
Copy link
Member Author

alexjbest commented Jan 12, 2022

#deploy
I guess cargo-culting github commands won't work for me :D

@gebner
Copy link
Member

gebner commented Jan 12, 2022

#deploy

@github-actions
Copy link

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

@alexjbest
Copy link
Member Author

Ok, https://leanprover-community.github.io/mathlib_docs_demo/init/core.html#or looks better now, I checked a few other inductives and they seem fine too.

@alexjbest alexjbest marked this pull request as ready for review January 12, 2022 20:00
@gebner gebner merged commit b337fdb into leanprover-community:master Jan 12, 2022
@alexjbest alexjbest deleted the fix_inductive_binder_types branch January 20, 2022 16:43
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.

2 participants