mlang icon indicating copy to clipboard operation
mlang copied to clipboard

Published 20 hours ago • verified publisher icon molikto

Implement `with_constructors` modifier

Open molikto opened this issue 5 years ago • 0 comments

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 avatar May 22 '19 04:05 molikto