Reed Mullanix
Reed Mullanix
## Patch Description This PR implements the start of a monoidal category solver, based roughly off of the ideas found in [1]. Specifically, we compute a normal form for each...
Right now we use the definition of morphism equality from `Function.Equality`, which is slated for deprecation in the future (see https://github.com/agda/agda-stdlib/issues/1467). Furthermore, there's a very good reason it's not recommended:...
### Description One of the biggest issues with GraphQL is that queries are very difficult to optimize, and may result in 1) Fetching the same data repeatedly 2) Inefficient fetches...
Template Haskell is a bit limiting, so I'm going to migrate to GHC API.
As it stands, quite a bit of the work involved in implementing new features is mucking around with odd TemplateHaskell representations. Using [th-desugar](https://hackage.haskell.org/package/th-desugar-1.9) could really cut down on a lot...
This has quite a few benefits. 1) We can have a custom quasi-quoter, which helps us both from an ergonomics and tooling perspective. This would enable the syntax: `tactic [thm|...
For example `apply '(+)` yields the error: ``` Tactic Error: lookupVarType: Variable Type ClassOpI GHC.Num.+ (ForallT [KindedTV a_6989586621679035072 StarT] [AppT (ConT GHC.Num.Num) (VarT a_6989586621679035072)] (AppT (AppT ArrowT (VarT a_6989586621679035072)) (AppT...
Sometimes, it helps to be able to label the subgoals, especially when handling inductive types like `Bool`. Implementation-wise, this is as easy as adding a `Maybe String` field to `Judgement`,...
Right now the code for freshening hypothesis names doesn't take into account cases where someone freshens something that ends in a number. This could cause name overlap, but is of...
When I originally made this project, I wanted to keep it pretty minimal, so C was the best option. However, in order to add features, quite a bit of string...