Eric Wieser

Results 473 comments of Eric Wieser

To an experienced user, I'd argue being able to spot a non-dependent binder at a glance is more valuable than matching pen and paper mathematics, but I understand the pedagogical...

I hadn't thought of recreating the account.

> Wait, what happened to https://github.com/brombo ? He asked GitHub to delete his account, along with the repo and open issues, as he forgot the password and the email address...

I went ahead and made the org page, that seemed easier than asking github to create the redirect: https://github.com/brombo/galgebra

> They already do this for repos that are moved. I'm pretty sure this becomes invalidated once someone creates a new user with the same name. The redirects are there...

Or if `o` is actually body rate, then ``` Vr = cross(o,D(:,i)) + inv(R) * v; ```

Thanks for doing that test. What does the conversion between the various types of grammar file? Could it be a bug that applies only to `json` grammars (https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json) and not...

Thanks for the further investigation. I think you're right that the `tmLanguage` vs `json` format is irrelevant, but I still think this is a bug in the grammar application, not...

@Alhadis is spot on - I found that if I removed either `Prop|` or `|Sort` from the example in https://github.com/github/linguist/issues/5069#issuecomment-716606285, everything works.