Trebor Huang

icon indicating a website link https://trebor-huang.github.io/

icon location Internal cat of a doughnut icon location I'm an undergrad at Tsinghua University. / I like mathematics and dependent type theory.

Results 72 comments of Trebor Huang

What's this?

And yes it will contain a typechecker, :(

Minor issue on naming

Maybe just go with Classical CuTT. In symbols, ¬¬||🧊||

Weird vibrations on iOS distro

This is impossible to implement without changing the source code of love and introducing undocumented API's of Apple, breaking support on older iOS versions.

Weird vibrations on iOS distro

> I'm pretty sure it's possible to check the OS version on LOVE, and you can adjust it to that No, the change of code is done outside of this...

Weird vibrations on iOS distro

Good news! We're working to do exactly the change I've described. But removing that slider before the work's done seems reasonable.

Weird vibrations on iOS distro

Should this be closed?

[ new ] explicit polarity annotations

IMHO `--polarity` is slightly too vague, can we have something like `--polarity-modality` instead? Or is that too long?

[MU4 Issue] Setting notes invisible crashes the program

More specifically: 1. Create a new score without changing any parameters. 2. Click the dotted note icon. 3. Place the note C4 and E4 on the first beat, in that...

[MU4 Issue] Setting notes invisible crashes the program

I'm on M1 if that is relevant.

Unicode superscript subscript not to be treated as identifiers in maths

I would like to suggest the opposite feature: allow all unicode sup/subscripts in variable names, which means forbidding the usage of `M₂` as mathematical formulas, and you have to write...