Hillel Wayne

Broken syntax highlighting after the first submodule

1

``` ---- MODULE foo ---- ---- MODULE bar ---- Op1 == TRUE ==== Op2 == TRUE ==== ``` Highlighting will not cover `Op2`.

Lean Proof Link Doesn't Work

1

It's because it uses a lemma from the Lean4 std (`nat.sub_add_eq_max`) but the online prover is running Lean3

This is extremely good

1

That's all

Explain limitations on arithmetic better

1

Provide the example of `#univ` in the evaluator

I don't know what features exactly this is gonna get us but I've fallen behind on these kinds of upgrades before and *do not* recommend it

Come up with good exercises

1

Now that there's an [exercise directive](https://github.com/hwayne/learntla-v2/blob/master/docs/_extensions/exercise.py) I can start putting exercises in the text. What are some good ones? Feel free to drop them here and I'll add some I...

Documentation update: Explain what makes ahkpm useful

3

Most AHK users haven't heard of a package manager before. What does this do for them? Is this for getting new APIs and libraries, or for getting new useful scripts?...

Can I embed this in another website?

1

1. This is amazingly cool, thank you for making this. 2. If possible, I think this would be a great addition to learntla. Is it something I can embed in...

Feature request: get list of references in project

2

It would be really helpful if I could use telescope to jump straight to a reference, like `.. _operators::`. I tried using telescopes `builtin.lsp_workspace_symbols` but I got the error >...