cooltt

cooltt copied to clipboard

## Patch Description This is a little PR that adds a `#debug` directive that toggles the debug mode on and off via `#debug on` and `#debug off`.

TOTBWF

ralsei

jonsterling

## Patch Description This PR adds a first-class notion of telescope, and unifies ## Motivation Right now, we have some Cool tricks for records; namely record patches [#274] and total...

TOTBWF

🚧 🦆 Inductive Types

3

TOTBWF

TOTBWF

vim plugin doesn't work with neovim

1

Hi, apparently neovim doesn't ([and won't](https://github.com/neovim/neovim/issues/8547)) implement the vim 8 job feature which the vim plugin uses. Instead it seems to have [it's own job control API](https://neovim.io/doc/user/job_control.html). I don't know...

rachelambda

[🚫 🐞] Improved Debugging Output

1

It would be nice to improve the `Debug.print` output a bit, and implement a `#debug` directive (I thought I had done this, but apparently not??)

TOTBWF

Problem with patching and names

3

Not sure what is going on here, but consider the following example: ````cooltt def category : type := sig def ob : type def hom : sig [s : ob,...

jonsterling

As it currently stands, the new `hcom_chk` tactic as given in #386 is the only one with the behavior such that: - When the boundary is satisfied, don't drop a...

ralsei