Julian Berman

feat(Multiset): add two lemmas relating Multiset.filter / Multiset.prod

1

--- (I definitely have not internalized the Lean4 naming conventions fully, so it's possible the names need tweaking.) I also think there probably is a more general version of the...

For monitoring, we'd want to send off the number of queued events (and to a lesser extent their size considering afkak can batch off that as well), but right now,...

Bind escape and q to exit without running anything

1

This adds a key binding for exiting the TUI via the same key bindings as closing modals. ISTM perhaps it'd be nicer for `escape` to be bound to work sort...

Create a JSON Schema Glossary Page or Site

15

It'd be nice if we had a glossary of terms -- a page, in not very technical jargon, which explains common terminology used by us in conversation, and which could...

Sphinx inventory is missing for UJS

8

This link: https://json-schema.org/understanding-json-schema/objects.inv on the old website was a [Sphinx inventory](https://www.sphinx-doc.org/en/master/usage/extensions/intersphinx.html) for Understanding JSON Schema. It now appears to be a 404. I know we don't plan on sticking with...

Given `foo` containing: ```python #!/usr/bin/env python3 from click.shell_completion import CompletionItem import click class Foo(click.ParamType): def convert(self, value, param, ctx): return value def shell_complete(self, ctx, param, incomplete): return [ CompletionItem(value=value, help="adsf")...

Sometimes a schema contains annotation-only keywords (particularly e.g. `description` or `$comment`) which effectively serve no purpose when reporting validation errors and essentially make the output longer / harder to read...

### Checks - [X] I have read the FAQ section, searched the open issues, and still think this is a new bug. ### Describe the bug you encountered: If one...