RedPRL/cooltt

Issues

• Nix Flake: No matching version for bwd >= 2.1

  #400 opened a year ago by solomon-b
  2

• 📛 Symbol.pp -> Symbol.dump?

  #210 opened 2 years ago by favonia
  1

• 💢 Tighter integration with GitHub Actions

  #321 opened 2 years ago by favonia
  1

• 🐫5⃣ Meta-issue for OCaml 5 support

  #330 opened 2 years ago by favonia
  2

• ⌨️ Add `deftype`

  #381 opened 2 years ago by TOTBWF
  5

• vim plugin doesn't work with neovim

  #397 opened 2 years ago by rachelambda
  1

• [🚫 🐞] Improved Debugging Output

  #394 opened 2 years ago by TOTBWF
  1

• Problem with patching and names

  #387 opened 2 years ago by jonsterling
  3

• Make hcom, com, coe, et al Chk tactics

  #393 opened 2 years ago by ralsei
  0

• Deep patching

  #390 opened 2 years ago by jonsterling
  0

• :selfie: JSreflect

  #389 opened 2 years ago by favonia
  0

• Global.t index is not unique across code units

  #379 opened 2 years ago by jonsterling
  1

• :no_good: <Something> should not compare names

  #377 opened 2 years ago by favonia
  7

• Readme install not working cleanly on Macos

  #287 opened 2 years ago by briangmilnes
  5

• Installing Cooltt in NixOS

  #302 opened 2 years ago by guilhermehas
  2

• 🧞 Remove the hash from the grammar (if mathematically possible)

  #329 opened 2 years ago by favonia
  1

• ⛳ Show numbers of holes

  #344 opened 2 years ago by favonia
  3

• 🧞 Document the grammar for non-genies

  #328 opened 3 years ago by favonia
  1

• :cd: Remove sigma types from the core language; use records

  #368 opened 3 years ago by favonia
  0

• 📥 Some thoughts about making it cooler to work with the total space of type family

  #348 opened 3 years ago by mmcqd
  2

• 📥 Auto-inserting `.fib` projections when the `fib` field is a record

  #366 opened 3 years ago by mmcqd
  0

• 🧦 Splice Linter

  #300 opened 3 years ago by TOTBWF
  3

• 🪡 Infer the value of patched record fields

  #326 opened 3 years ago by mmcqd
  1

• 📌 Keep location information in ConcreteSyntax.decl

  #316 opened 3 years ago by favonia
  0

• Move constructors of `decl` which are actually commands to `command`

  #317 opened 3 years ago by favonia
  0

• 🆔 Introduce `!def` and make `def` non-shadowing

  #319 opened 3 years ago by favonia
  1

• ⛳ Move the parsing of hole names back to the LR(1) parser?

  #252 opened 3 years ago by favonia
  1

• 🚫🆔 Nameless schemes for `BindSym`, `LetSym` and `DimProbe`?

  #335 opened 3 years ago by favonia
  0

• ↔️ `equate_*` returns a cofibration under which the two terms are equal

  #334 opened 3 years ago by favonia
  0

• 📥 Support for auto-converting between fibered and parameterized type families

  #267 opened 3 years ago by jonsterling
  4

• 🧞 Pretty printing for signatures and structures

  #331 opened 3 years ago by jonsterling
  0

• ↔️ Equational Reasoning DSL

  #304 opened 3 years ago by TOTBWF
  1

• 💥 Tear down the multi-layer build system

  #310 opened 3 years ago by favonia
  0

• ⚠ Remove deprication warnings from Cmdliner

  #307 opened 3 years ago by favonia
  0

• ☣️ Issue dispatching hcom for sigma types

  #303 opened 3 years ago by TOTBWF
  4

• 🍱 `open ContainersLabels`

  #206 opened 3 years ago by favonia
  0

• 🪡 Record patching (like SML `where type`)

  #266 opened 3 years ago by jonsterling
  2

• Proposal to extend boundary-sensitive refinement to positive types

  #297 opened 3 years ago by jonsterling
  2

• Capture bug in implementation of dimension substitution

  #288 opened 3 years ago by jonsterling
  0

• 🦆 Inductive Types

  #282 opened 3 years ago by TOTBWF
  1

• #️⃣ Prefix commands with a hash

  #277 opened 3 years ago by TOTBWF
  0

• 💔 Testing is broken

  #270 opened 3 years ago by favonia
  10

• 📑 CITATION files

  #264 opened 3 years ago by favonia
  1

• 🚰 filler-of tactical?

  #259 opened 3 years ago by cangiuli
  5

• 🇿 Auto-completion for zsh

  #261 opened 3 years ago by favonia
  0

• Tests don't run anymore

  #240 opened 3 years ago by jonsterling
  14

• Preserve names during normalization

  #244 opened 3 years ago by TOTBWF
  0

• It is no longer possible to run the tests

  #209 opened 3 years ago by jonsterling
  1

• add dune task for ocp-indent?

  #208 opened 3 years ago by jonsterling
  6

• 🦯 De Brujin indexes/levels for `BindSym`, `LetSym` and `DimProbe`?

  #215 opened 3 years ago by favonia
  0