thorimur

Some symbols are only accessible by browsing through a list of symbols. For example, to input ►, one types `\t`, is presented with a list of different triangles, then presses...

Although an experienced Lean user will know to simply not name packages incorrectly, a new one might choose to name a package e.g. "meta" with `lake init meta`, then be...

This adds: * a module doc for `Lean.Elab.StructInst`, which gives an overview of how the code for structure instance elaboration works * docstrings for each definition in `Lean.Elab.StructInst` Note: I'm...

fix: handle delayed-assigned mvars in `isDefEq` safely

3

Currently, unknown fvars can be introduced during `isDefEq` when synthetic opaque metavariables are assignable and appear in a delayed assignment. Specifically, if `?m.23` is delayed-assigned to `?a`, we currently replace...

fix: `isDefEq` handling of delayed-assigned mvars when `withAssignableSyntheticOpaque` is `true`

2

(In progress; fully experimental.)

(experimental) fix: match `MonadControlT` to `MonadControl`

1

Experimental draft PR to utilize CI. Experiments with changing the `MonadControlT` interface on the basis of [this zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/MonadControlT.20vs.20transitive.20closure.20of.20MonadControl) to see if it makes sense to open an issue.

feat: adjust `dsimp` behavior (experimental)

1

This is an experimental draft PR to assist with #2679 which exists solely to utilize CI.

bench: lean4#3473

2

--- [](https://gitpod.io/from-referrer/)

feat: indent on enter after certain EOL tokens

4

This PR causes indentation when hitting enter after certain tokens that appear at the end of a line. Specifically, after: * `by`, `do`, `try`, `finally`, `then`, `else`, `where`, `extends`, `deriving`,...

feat: make `registerLabelAttr` consistent with `registerTagAttribute`

4

This PR modifies the recently-upstreamed `LabelAttribute`s to be consistent with `TagAttribute`s. Specifically, we modify `registerLabelAttr` to * allow a `validate` argument * allow an `AttributeApplicationTime` argument * change the default...