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.

Sign up for GitHub

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

Jump to bottom

map num to N (binary naturals) #6

Closed

fblanqui wants to merge 8 commits into Deducteam:main from fblanqui:binnat

Member

fblanqui commented Jan 11, 2025 •

edited

Loading

TODO:

check that HOLLight.v in hol2dk works
map Even and Odd
map LENGTH
map REPLICATE

fblanqui added 8 commits

January 11, 2025 15:01


          map num to N (binary naturals)

53373a0

wip

6844f29

wip

4e3477f

wip

wip

ff0796b

wip

bb219ab

wip

03aa4be

wip

bcea7ab

Member Author

fblanqui commented Jan 13, 2025

moved to https://github.com/Deducteam/coq-hol-light-real-with-N

fblanqui closed this

fblanqui deleted the binnat branch

January 13, 2025 16:05

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet