Reed Mullanix
Reed Mullanix
## Motivation Currently, the only way to define types is via `def foo : type := ...`, which has some interesting ramifications regarding fibrancy. In particular, we can't define record...
When constructing things inside of the splicer, it's easy to make mistakes and accidentally produce ill-typed terms, which can be really hard to debug. This is _especially_ true when dealing...
When messing around with some ideas that @cangiuli had regarding records, I came across the following crash: ```cooltt import prelude import hlevel -- Equivalences. def fiber (A : type) (B...
## Basic Design + Syntax The (rough) syntax for defining an inductive type is as follows: ``` data type-name (x1 : p1) (x2 : p2) ... : (y1 : i1)...
## Patch Description This PR adds 2 new functions to containers: `Data.Map.between`, and `Data.Set.between`. These functions will consume a map/set (respectively), and will filter the map/set so that the keys/values...
The `insMapEdge` family of functions are partial, and will crash when you try to add an edge where one of the nodes doesn't exist in the graph. This doesn't appear...
I'm looking into bringing `ocaml-lsp-server` up to date with the recent OCaml 5 changes, and I noticed that `dune` is being vendored so that we can heavily patch `ocamlc_loc`, and...
Right now, the output of `fsharp/documentation` is very ionide specific. For example, consider: ```json { "XmlKey": "M:Microsoft.FSharp.Collections.SeqModule.TryFind``1(Microsoft.FSharp.Core.FSharpFunc{``0,System.Boolean},System.Collections.Generic.IEnumerable{``0})", "Constructors": [], "Fields": [], "Functions": [], "Interfaces": [], "Attributes": [], "Types": [], "Signature":...
# Description This PR implements Preadditive categories, in the style of Borceux1. We also prove some properties, the most interesting of which surrounds biproducts. Traditional definitions of biproducts often require...
Currently, `RegularEpi` and `RegularMono` are defined like so: ```agda record RegularMono (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where field { C } : Obj...