Reed Mullanix

Webpage Generation

3

Closes #3

chore: add page for tracking Borceux progress

1

# Description Adds a page for tracking progress on Borceux. Somewhat surprisingly, we are already 34% of the way done! ## Checklist Before submitting a merge request, please check the...

Add new `PostponedTerm` type to reflection API

6

## Motivation Occasionally, have some `Term` argument to a macro whose type we want to compute in the body of the macro. As an example, consider a macro that repeatedly...

Port defadvice to define-advice

3

As of Emacs 30.1, `defadvice` has been marked obselete, and can lead to byte-compilation errors. Luckily, this is easy to fix; all we need to do is to replace invocations...

Allow selective record eta rules via `unfolding`

6

Eta-rules for record types are extremely useful, but don't come for free. They can be the source of pretty serious performance issues, and can also make your goals nigh-unreadable if...

# Description Doing a bit of point-set topology for Borceux/taboos. ## Todos - [ ] Finish writing prose: in particular, the introduction needs to be much better. - [ ]...

Rename `Bwd.append` to `Bwd.append_list`

2

Currently, `Bwd.append` has type `'a bwd -> 'a list -> 'a bwd`; this isn't consistent with the API for lists, which has a homogenous `List.append : 'a list -> 'a...

See #31 for discussion.

Grammar for postfix projections is a bit too forgiving

2

Agda is pretty forgiving when it comes to whitespace and postfix projections. ```agda module Postfix where postulate A : Set record R : Set where field proj : A open...

Improve module checkpointing performance

6

I was doing some profiling of agda against `1lab` builds the other day, and noticed that we were spending upwards of 5% of our time inside of the `Ord` instance...