redtt

redtt copied to clipboard

Factor out Favonia Namespace code into library

3

For now, just a local library in this repository.

jonsterling

Mortality

6

ncoe too mortal `split/half` on line 260 [https://github.com/RedPRL/redtt/blob/mortal/library/cool/sort.red](https://github.com/RedPRL/redtt/blob/mortal/library/cool/sort.red) `raise TooMortal` on line 347 [https://github.com/RedPRL/redtt/blob/mortal/src/core/Domain.ml](https://github.com/RedPRL/redtt/blob/mortal/src/core/Domain.ml)

kaonn

Currying inside systems

1

For this definition ``` def comp3 (A : type) (b : (j0 j1: 𝕀) → A) (k0 : [j1 k] A [ k = 0 → b 0 j1]) (l0...

3abc

smalltt

1

This is apparently very fast. Are any of the ideas useful in redtt? https://github.com/AndrasKovacs/smalltt

spitters

WIP Diaconescu's theorem

12

Currently I'm stuck defining the `P` family in `suspension-lemma` for the double `merid` case :(

clayrat

Resolution of constructor names

2

# Proposal `NameRes` should associate each constructor name to a list of `{datatype : Name.t; clbl : string}` which represents all possible interpretations. This will automatically support renaming, namespaces, shadowing,...

favonia

Option support request

6

- [ ] `--allows-empty-system`: no ghcom etc - [ ] `--fhcom-kan=?`: try different implementations of fcom ~and V~ types. - [ ] `--paranoid`: normalize everything extremely eagarly - [ ]...

favonia

System rectification campaign

5

All of these should be implemented. This applies to compositions, extention types, and boundaries of constructors. @jonsterling @cangiuli @ecavallo - [ ] False removal: remove any false faces as soon...

favonia

**Spoiler Alert**: there are no _private_ data types right now!

favonia

Syntax and semantics of namespaces

1

- [ ] enrich ResEnv to enable local opens and prefixing - [ ] implement the keywords `open` and `namespace`, sharing the code with #449. - [ ] implement the...

favonia