Andrea Vezzosi

Reduction missing during LHS checking

3

Regression introduced by fix of #2964 (making LHS matching stricter), similar to #2968. ```agda module _ where open import Agda.Builtin.Equality open import Agda.Builtin.Sigma open import Agda.Builtin.Bool T : Bool →...

I think a `Foo` module should export what you're more likely to need about `Foo`. If they re-export everything that's been developed for `Foo` then they are not as useful...

Ideally we would test against Reference.termToJson. _Originally posted by @Saizan in https://github.com/well-typed/cborg/pull/315#discussion_r1179092023_

List holes and other errors separately.

1

When ghci lists the number of errors it includes the `Found hole: ...` ones. Unfortunately the error messages tend to be quite large, so if I have enough holes it's...

[fix #15] ChatFunctionCall arguments field typed as Text

3

Here's a fix for issue 15, just changing the type of the field and the To/FromJSON instances.

The arguments field of a function call object is not guaranteed to be valid JSON, here's the relevant quote from the API reference ``` The arguments to call the function...

When doing requests in parallel it's not too hard to hit rate limits: https://platform.openai.com/docs/guides/rate-limits Would be great to have rate limiting support, e.g. across all clients generated from the same...