Ed Ayers

I have a deployment that depends on [kafkasaur](https://deno.land/x/[email protected]). It connects and runs correctly on my local machine, but when it runs in deno deploy I get an error message ```...

feat: utilities for using scientific notation and floats in json

2

- [x] waiting on https://github.com/leanprover/lean4/pull/1460 to include a `JsonNumber.fromFloat`

RFC: Contextual suggestions

24

# RFC: contextual suggestions  People who are probably interested: @KaseQuark @Kha @javra @Vtec234 @leodemoura @gebner ## Links - [prototype Lean code](https://github.com/Vtec234/npm-widget/blob/5cb1e41aa2a2f597c7821c7b7873316da822ff49/UserWidget/ContextualSuggestion.lean) - [prototype vscode-lean4 code](https://github.com/Vtec234/vscode-lean4/blob/6ab8a5b60c3faca3ed2e1a3674b822ce98e0d08a/lean4-infoview/src/infoview/contextualSuggestions.tsx) ## Goal The purpose...

feat: deriving optics

2

This file defines the `derive_optics T` command where `T` is an inductive datatype. For each constructor `𝑐` of `T` and each field `𝑎 : α` of `𝑐`, this will create...

feat: profunctor optics

2

A port of some of https://hackage.haskell.org/package/profunctor-optics-0.0.2/docs/Data-Profunctor-Optic-Traversal.html Just for fun. ## How should composition work? If anyone has a good idea for how to get optic composition to work smoothly I'd...

`norm_num` needs to support - ``, `≠` - Ring operations: `Neg`, `Sub`, `%` - Field operations: `/`, `⁻¹` - Reals and rationals

doc(tactic): add explanation of approx for unify

1

I've always wondered what that flag did...

Lean server produces hundreds of "checking import for sorry" tasks

2

I am using `Lean (version 3.16.5, commit 101e2ca571cc, Release)`. I am using vscode 0.15.15, commit 7b5d8717f79d. I think it is something weird about the project I am working on because...

Settings dialogue doesn't work on gtk4 / Gnome 40

15

This issue stems from #190 Gnome version: 40.0.0 Windowing system: X11 OS: Arch Linux, rolling There is a problem, the extension itself is working for me but I've discovered the...

I'm not completely sure what the right API would be. It would be nice to be able to have something like `inputFileTarget` but to specify a directory for whole directories....