On Fri, Jun 4, 2021 at 5:42 PM Arun Sharma <arun@sharma-home.net> wrote:
On Fri, May 28, 2021 at 11:01 AM Arun Sharma <arun@sharma-home.net> wrote:
A variant of this syntax and a proof of concept implementation built on top of adt [1] library:
The upstream ADT library has some mypy plugins. Would be great if other type checkers supported something like this out of the box.
-Arun
This syntax is now supported in the python -> rust transpiler. Test case in this commit:
Also supported in the python -> smt transpiler as of: https://github.com/adsharma/py2many/pull/443/files Some links about python and SMT: https://ericpony.github.io/z3py-tutorial/guide-examples.htm http://smtlib.cs.uiowa.edu/ Compare: ; smt-lib2 (declare-datatypes ((IntList 0)) (((None) (intlistnonempty (first Int) (rest IntList))))) or # z3py # Declare a List of integersList = Datatype('List')# Constructor cons: (Int, List) -> ListList.declare('cons', ('car', IntSort()), ('cdr', List))# Constructor nil: ListList.declare('nil') The sealed classes feel a lot more natural to write. -Arun