Vojtěch Štěpančík
Vojtěch Štěpančík
I like what the cubical people do with https://agda.github.io/cubical/Cubical.Papers.Everything.html, where they have a module per publication, and then import the constructions/lemmas/results from the actual library.
This issue is blocked on https://github.com/lzanini/mdbook-katex/issues/93, which in turns needs https://github.com/rust-lang/mdBook/issues/2179.
> I just think that from a maintainers perspective, it is not good to let Agda dictate what arguments should be implicit based but we should make that decisions as...
I think the idea here is to be able to implement it in the log function only, without the caller having to provide the `@src()` argument.
I will submit a PR once the mentioned mdbook issue is solved 👍
> Are you unable to type this symbol using the sequence `cdot`? I'm not at my computer anymore, but I tried looking through all the symbols I could type with...
> The website uses the following series of fonts in prioritized order (decreasing) to display agda code: > > ```css > font-family: Menlo, Source Code Pro, Consolas, Monaco, Lucida Console,...
I tried to find out how the different fonts used for the website show the two symbols, and this is what I found (I think some of the fonts don't...
FWIW to find out what font Brave (or other chromium-based browser) uses for a chunk of text, you can select the text, right click -> inspect -> switch the side...
Related to #768. I remember discussing this with Egbert in September '23, where we identified two issues: 1. printing those things in goals is finicky. If the syntax is an...