Víctor López Juan

Searching "TEST" on Google redirects to the following when Startpage.com is selected: https://startpage.com/search/?q=TEST That URL used to work, but now redirects to the homepage. I believe that the search should...

Hinting quirks for 'x', '→' and others in 10pt, aliased

1

I use PragmataPro with no antialiasing at 10pt size (sometimes 11pt). I find it good in general. However, the hinting for some symbols seems to have gotten worse in recent...

Project heterogeneous constraints (v2)

23

This pull request supersedes #4605. ## What? Constraints in Agda are currently of the form: `Γ ⊢ t ≈ u : A` These constraints are homogeneous, which means that: -...

I have had issues with `hasktags` and emacs when involving literate files in Bird notation E-macs version: 26.1 Consider a file like this: ```lhs This is foo: > data Foo...

Support quoted strings

1

The last ASCIIMath version supports using quotes to delimit `text` elements, like so: Input: ``` "time" = "money" ``` Result: ``` html time = money ``` This commit brings the...

Add specialization of `retract` for `Iter ~ IterT Identity`

2

When using the `Iter` monad, it is common to, at some point, run the computation until it terminates by using `runIdentity . retract`. This could be implemented as a separate...

Expose intent to create node

1

It would be useful if one could share, say, a webpage from the web browser to syncorg, and easily create a node out of the URL and title.

Allow implicits for mixfix operators

2

Here is a proposal: https://gist.github.com/vlopezj/1de925406d10eba30f6fd849ed174917 TL;DR: Implicits would appear to the right of the part of the mixfix operator they fall under. In particular, this means that sometimes the arguments...