Fredrik Bakke

`C-c` `C-s` and `C-c` `C-a` inserts `\n` instead of newlines

3

What the title says. For instance, in the following case Using `C-c C-s` will give For this issue to be resolved, #159 should probably be resolved first, as otherwise the...

Holes spanning multiple lines are not handled (in literate files)

8

Holes spanning multiple lines are not highlighted: And attempting to insert using `C-c C-space` does not work:

Nested holes are highlighted only from the first opening to the first closing bracket. Example:

Built-in sorts are highlighted as strings

1

Built-in sorts are highlighted as strings, but shouldn't be: I suggest using a scope like `support.type.sort.agda` instead.

Various symbol additions to agda-input

3

This PR adds a range of symbols to `agda-input` including - Non-alphanumeric fullwidth symbols - Boxed operators `⧄⧅⧆⧇⧈` - Esh `ʃ` - At `@﹫＠` The boxed circle operator introduces a...

Noncoherent wild (∞,∞)-precategories

4

- Large and small noncoherent wild $(∞,∞)$-precategories - maps of globular types - maps of noncoherent wild $(∞,∞)$-precategories - Colax functors of noncoherent wild $(∞,∞)$-precategories - Induced colax functor on...

Displayed precategories

1

Defines displayed precategories.

Rewrite rules for pushouts

5

### Todo - [ ] Wait for #885 to merge. - [ ] Refactor postulates of universal properties to be phrased in terms of coherently invertible maps. - [ ]...

Basic properties of the flat modality

6

This is the replacement of #1005. Proves a series of basic properties of the flat modality. ## Summary ### General properties - [X] The universal property of flat discrete crisp...

Colocal types

1

Defines what it means for a type to be colocal at a map, and shows a few basic properties of these.