Reed Mullanix
Reed Mullanix
F# has no implicit upcasting, requiring either a direct cast using `:>` or the `upcast` keyword. This causes issues when trying to use the Linq update, as it requires a...
### Thank you for the bug report - [X] I am using the latest version of `lsp-mode` related packages. - [X] I checked [FAQ](https://emacs-lsp.github.io/lsp-mode/page/faq/) and [Troubleshooting](https://emacs-lsp.github.io/lsp-mode/page/troubleshooting/) sections - [ ]...
See [this.](https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Foldable.html#v:traverse_) This function is can be super handy when writing lens combinators.
Fixes #150 and #149. Previously, changes to non-`Main` purescript files would not trigger hot reloading. This is because the files were not registered with `addDependency`, so they didn't trigger rebuilds....
## Description This PR adds an interactive function for performing case splits. To use it, simply place your cursor over a typed hole, and call `lsp-haskell-case-split`. You should be prompted...
Right now, we define function setoids as follows (taken from [Function.Equality](https://github.com/agda/agda-stdlib/blob/master/src/Function/Equality.agda#L79)): ```agda setoid : ∀ {f₁ f₂ t₁ t₂} (From : Setoid f₁ f₂) → IndexedSetoid (Setoid.Carrier From) t₁ t₂...
# Description This PR proves [Duskin's Monadicity Theorem](https://ncatlab.org/nlab/show/monadicity+theorem#duskins_monadicity_theorem), and also provides the associated machinery. This closes #74. I'm also proving the version found in the Handbook of Categorical Algebra ##...
When doing stuff with integers, it's pretty common to see some really gnarly goals involving nats. For instance, this monster comes up when you try to define integer multiplication ```agda...
In order to round out our monadicity theorem collection, it would be fun to prove [Duskin's Monadicity Theorem](https://ncatlab.org/nlab/show/monadicity+theorem#duskins_monadicity_theorem). There are a couple of variantions on this, but the following version...
Right now we have a notion of preservation/reflection of (co)limits that works over limit diagrams, but this is often a bit annoying to work with when we are working with...