cooltt

cooltt copied to clipboard

I think we don't support deep patching, as in `S # [foo.bar := baz]`; nonetheless, this is a useful and important feature of ML-style module systems that could be nice...

jonsterling

Extract the ssreflect API to a standalone OCaml library

favonia

To speed up the development of the next generation of cooltt, I propose turning isolated components into more OCaml packages ~~with anime-inspired names~~. Here are some ideas: - [x] Namespaces:...

favonia

⌨️ Add `deftype`

5

## 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...

TOTBWF

Serialization and imports

3

See, for example, what @favonia did in redtt.

cangiuli

favonia

Consider returning to strict universes

6

I had decided to use cooltt to experiment with weak universes, i.e. universes where the decoding laws hold up to iso. These are fine, but they make certain things harder...

jonsterling

Once #361 gets merged, I want to consider ways to auto-insert `.fib` projections even in the case where the `fib` field is a record. This becomes a problem as soon...

mmcqd

🧦 Splice Linter

3

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...

TOTBWF

Elim on a variable already in the context?

1

@jonsterling

favonia