Tej Chajed

Glad you found an answer yourself! This is pretty tricky to support correctly. We don't currently need it, but might eventually want recursive structs (although not mutual recursion). The good...

I had not intended to support recursive functions, so thanks @upamanyus! (The translations use `rec:` so that the interpreter can produce a trace of functions called, which was useful for...

This will break an Iris proof mode feature that goes from a Gallina string to an identifier (through an Ltac2 string and an Ltac2 ident), hence the failures in Iris...

Indeed the behavior is as intended but the README is admittedly confusing. It should explain that "`setAB`" is really updating both fields in terms of their old values, whereas `setAB'`...

Yeah, lenses make a lot of sense in conjunction with this library. It shouldn't be hard to define and implement lenses on top of the `Setter` typeclass, and then let...

I implemented something in ca0fe8ef47fd95c99ab3241abf0e4f61ad6dd357 - it's really just your definitions of lenses and lens composition, with a way to definition that turns a projection function into a lens using...

@amblafont if you want to work on this a starting point is `docker buildx build --platform=linux/amd64,linux/arm64 .`, which uses the [buildx plugin](https://github.com/docker/buildx) to do a multi-arch build. I think this...

My guess (because I had the same bug) is that you need to use a capturing group in your regex: ```ts let el = reactStringReplace(el, /(\n)/g, (_match, i) => );...

You can fix the CI failure by bumping the revision in the math-comp formula (see #135135 for an example).

I didn't intend to support this, so it should probably be rejected for now. It's a bit unfortunate since this is idiomatic Go and the alternative won't be as easy...