Jannis Limperg

@treeowl: If I understand the [process](https://wiki.haskell.org/Library_submissions#Guide_to_proposers) correctly, a proposal should start out with an issue on the tracker; this is that. @foxik: For what it's worth, I did not see...

I have a fix for this, but I don't have the necessary rights to push to this branch yet. @digama0 could I get these?

I replaced your API for `modifyLocalContext` etc. with an API that is arguably more in line with the core APIs, though whether that makes it better is another question. Feel...

Yes. The advantage of my API is that it works for any `MonadMCtx` and does not need to create additional metavariables. But there's certainly a tradeoff here. If you put...

I'm not actually sure that this is a good idea, because of the meta issue. For meta types like `name` and `expr`, this instance is fine, but for non-meta types,...

[`revert_deps`](https://github.com/leanprover-community/mathlib/blob/f9f0ca6d1a5438018e4611f372bbd5e47ee2a055/src/tactic/core.lean#L465) could also be a candidate. It works like `revert_kdependencies`, but takes the bodies of local definitions into account. It would have to be generalised a bit to properly replace...

I'm finally getting to this, sorry for the very long wait. Looking at how to best implement this, I'm quite confused by all these different unfolding methods. My understanding so...

Fair question. At the moment, your only choice is to write a wrapper macro that calls Aesop with specific options. But I think it would make sense to use the...

I'm afraid I can't reproduce. My test setup: `lean-toolchain`: ```text leanprover/lean4:nightly-2022-10-03 ``` `lakefile.lean`: ```lean import Lake open Lake DSL package repro { -- add package configuration options here } @[defaultTarget]...

Can't reproduce this either -- I can open `Repro.lean` in VSCode and Emacs and it typechecks without issues. My best guess is that your environment got subtly broken somehow, so...