Trebor Huang

Minor issue on naming

4

In case you want to change it early, "classic" is [far from old enough]((https://english.stackexchange.com/questions/48608/difference-between-classical-and-classic)) to describe a kind of logic :P Maybe it should be switched to "classical".

[MU4 Issue] Setting notes invisible crashes the program

8

**Describe the bug** Setting notes invisible crashes the program **To Reproduce** Steps to reproduce the behavior: 1. Create a score 2. Place a dotted chord directly 3. Set a note...

Better default spacing for matrices

8

### Description Currently, you can customize matrix spacing as per #1696. But the default spacing (hardcoded with em units) only works well for the usual font sizes. Since smaller fonts...

`RecordEquiv` reflection doesn't seem to handle implicit field arguments

6

MWE: ```agda {-# OPTIONS --cubical #-} module test where open import Cubical.Reflection.RecordEquiv using (declareRecordIsoΣ) postulate Bar : Set Baz : Bar → Set record Foo : Set where field foo...

Slightly more generalized universes

1

https://github.com/agda/cubical/blob/132a2a3197b490c571356f0399a2a6fbfab40f2a/Cubical/Foundations/Transport.agda#L170C1-L170C1 This could be slightly improved with `∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}`. It's too trivial so I won't submit a PR here. Also we...

See https://github.com/cliffordfajardo/highlight-line-vscode/blob/master/src/extension.ts

See if VSCode fonts can be used

- In project? - Globally?