Atticus Kuhn
Atticus Kuhn
I also encountered this same error. Here's what I did: 1. Ran `lake new lean_test math` 2. Opened the file `Basic.lean` in Emacs 3. Tried the command `lean4-toggle-info` 4. Got...
relevant: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20The.20connected.20server.28s.29.20does.20not.20support.20method.20.24.2Flean.2F.2E.2E.2E Maybe this issue is related to Doom Emacs?
I broke up `Cartesian` into `Monoidal`, `Braided`, and `Symmetric`. The heirarchry before was `Category` -> `Cartesian` -> `CartesianClosed` Now, it is `Category` -> `Monoidal` -> `Braided` -> `Symmetric` -> `Cartesian`...
I hope I got all the laws for a monoidal category written down correctly. Here is what I have so far ```agda unitorᵉˡ∘unitorⁱˡ : ∀ {a : obj} → unitorᵉˡ...
Thanks for your feedback.
Great, thanks for your feedback.
I have one theory, which is maybe we should use ``` lake exe cache get! ``` instead of ``` lake exe cache get ```
By the way, "Compile `mlirnatural` Executable 🧐" takes up 58% of the total runtime of the github workflow, so this could possibly speed up the GitHub workflow significantly.
> @AtticusKuhn, are you planning to update this PR. It might be useful to get it merged such that it does not get out-of-date. Well, as I wrote this PR,...
cc: @alexkeizer because he knows a lot about the parser.