Siyuan Chen

Happy to attend (9pm China time is OK for me). Thanks! PS. I will summarize some thoughts in the Issue List these days (may be useful for discussion).

Which video conferencing software do you plan to use? You may need to adjust my network in advance. Thanks.

Zoom is OK for me.

Thanks for your great answers ! @namin @michaelballantyne . I have a lot of things like to write, but they are not well organized yet. I will add it later,...

About "Integrating equalities, disequalities, and types" This section gave me a lot of inspiration, thanks. I was thinking that it seems not a big problem if minikanren with SMT does...

> For example, in the interpreter equal? is applicable to many types of argument: strings (which do not use the solver), numbers (where we'd like to use the solver), and...

> In the all-diffo example, could you reuse the definition of equalo? Yes. ``` (define all-diffo (lambda (l) (conde ((== l '())) ((fresh (t v) (symbolo t) (== l `((,t...

> did you find it educational to read the canonical implementation before diving into faster-miniKanren? If it's just for hooking SMT, it doesn't seem no much difference (I now even...

> What examples have been tried? Which are interesting? I am reading the test cases these days. IMO, all the examples are interesting :) Here are some examples that I...

> It seems that z/reify-SM mistakenly grounds SMT variables. I mean z/reify-SM should ignore these grounded declares. See below. The initial motivation is that I'd like to write an `add1o`...