Liang-Ting Chen
Liang-Ting Chen
By the way, the output in Emacs does not contain these two kinds of information.
FontAwesome provides this icon as well, so probably removing this icon from academicons may resolve this issue for now. However, it appears to me that the license is not really...
This proposed syntax follows the current convention of `unquoteDecl` and `unquoteDef`, but in the presence of overloaded names, it becomes overly verbose and shows why the proposal in https://github.com/agda/agda/issues/5864 is...
It seems that @UlfNorell is currently not active. Maybe someone else (ping @nad, @andreasabel) would like to have a look before merging?
I am inclined to merge this PR in 7 days (Aug 15) if no one objects. 😝
It seems that our PR (#5978) breaks yours but I have merged ours into the master branch. I'd like to merge yours soon as well. If you don't have time...
> @WhatisRT or @L-TChen: We're planning to release Agda 2.6.3 by the end of October, do you think you have time to work on updating this PR before then? If...
Another issue I have in mind is whether the tactic used to define these declarations should take names as arguments implicitly. As an example, I have a patched Agda which...
For the record, during AIM XXXV we concluded that we plan to implement @andreasabel's proposal with tactics whose types are of the form ``` t₁ → t₂ → .. →...
What is the current status of this issue? There was a code sprint but I do not see any progress. @Zekt and I are working on reflection on datatypes, and...