Skip to content
This repository has been archived by the owner on Oct 2, 2021. It is now read-only.

Implement with_constructors modifier #4

Open
molikto opened this issue May 22, 2019 · 0 comments
Open

Implement with_constructors modifier #4

molikto opened this issue May 22, 2019 · 0 comments
Labels
help wanted Extra attention is needed

Comments

@molikto
Copy link
Owner

molikto commented May 22, 2019

the idea is define with_constructors nat = ... will define suc zero at the same level as nat.

currently they are used as nat.zero
@molikto molikto added the help wanted Extra attention is needed label May 22, 2019
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
help wanted Extra attention is needed
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@molikto