Anand Rao

I'm facing the same issue ("Press Enter to start Julia. Julia has exited"). I'm running Atom 1.51.0 on Windows 10, with julia-client version 0.12.6 .

I suspect that this may be because of [this line](https://github.com/leanprover-community/mathlib4/blob/cf2e683c25eba2d798b2460d5703a63db72272c0/Mathlib/Tactic/Ring.lean#L90) in the code. Right now, it seems conditional on the implementation of rational numbers in `Mathlib`.

This PR is ready for review. In a set of future PRs, we would like to introduce the following additional features: - [ ] More general syntax for referring to...

> To be honest, I'm not yet convinced that the new location syntax is needed, because if you want to do something at specific locations in multiple different hypotheses, then...

I have modified the `locs` syntax to something simpler that targets a single location. I think I am much happier with it in this form. I have updated the checklist...

The `replaceLocalLetDefEq`, `defineAfter` and `replaceLocalLetDecl` definitions in `Pattern/Location` are functions that may be of general utility, so I could also try to PR them to Lean core (say into the...

> I have code that allows these patterns to also include bound variables. Would it be better to add it to this PR or to put it in a later...

React supports an alternative way of specifying state update logic through [Reducers](https://react.dev/learn/extracting-state-logic-into-a-reducer). Instead of running arbitrary JavaScript code when an event - like `onClick` or `onHover` - occurs, reducers allow...

The built-in Lean type [`SubExpr`](https://github.com/0art0/lean4/blob/master/src/Lean/SubExpr.lean) may be useful here. A `SubExpr` is determined by a `SubExpr.Pos`, which is a type synonym for `Nat`; however, the function `SubExpr.Pos.toArray` decodes the `Nat`...

Closely related to targeted rewriting with `conv` [is this demo](https://github.com/EdAyers/ProofWidgets4/blob/cf2e6e09166e1e8d791f8435bf1e3769da2d5b86/ProofWidgets/Demos/Conv.lean) from the `ProofWidgets` repository. A variation of the `solveLevel` function might be what is required.