Tesla Zhang‮

The equivalent code works in Agda: ```agda open import Agda.Builtin.Nat wow : ∀ {ℓ ℓ'} {A : Set ℓ} {B : A -> Set ℓ'} (a b : A) (x...

> Allow constructors defined by pattern matching (as `vcons`). Maybe #142

We can don't support those cases. I agree that it's kinda pointless to put a goal there

I guess it tries to unify the two sides without trying to compute one of them.

That's not related to this inference problem. The proof can be simplified, and I'm aware of that

Not now, but thanks for your suggestion. We have a `Read`/`Write` trait support for reducing data copying, though.

Have you tried looking at the examples? Some of them are using client streams, are those what you're looking for? https://github.com/pingcap/grpc-rs/blob/fec97d193a2c25c43dc61db6e1d8716e17ee9dcf/tests/cases/cancel.rs#L153-L160

Thank you! Will look into this.

Question: what's your expected Rust API look like? Can you provide some examples? Ref: https://grpc.io/grpc/core/grpc_8h.html#a568bac9fe4004c1dd790e6569b918d2f Function description: > Watch for a change in connectivity state. Once the channel connectivity state...

Reference: https://stackoverflow.com/q/41856536/7083401