Andreas Abel
Andreas Abel
``` agda -- {-# OPTIONS -v scope:10 #-} data Bool : Set where true false : Bool postulate f : Bool → Bool g : Bool → Bool P :...
Until 2.5.3, this was a parse error: ```agda f : Set₁ → Set₁ f with Set ... | _ = λ _ → Set ... x = x ``` From...
I guess this concerns @plt-amy and maybe @jespercockx and maybe others... Labels that have been renamed on github must be renamed accordingly in our release tool _closed issues for milestone_....
On case-sensitive file systems, the following is legal Agda: ```agda import A import a ``` assuming files `A.agda` and `a.agda` are in the project root. However, this might lead to...
Andy Pitts reports that he would like to rewrite projections: ``` agda {-# OPTIONS --rewriting #-} infix 4 _↦_ postulate _↦_ : {A : Set} → A → A →...
@plt-amy : Please be conservative in the label colors. The colors of at least the old labels have been fitted for aethestics. E.g. these new different reds are dissonant:
The branch parametric does not build under ghc 8.6. It would be good to keep agda-parametric alive; we have submitted a paper that relies on it. :)
Emacs command `C-x r t` (`string-rectangle`) is not executed in the Agda input mode, but in the plain input mode. Currently, a manual switch back to the Agda input mode...
We had commit tag `[complete tests]` for the Travis CI that would run the tests on all builds (as opposed on only the build with the latest GHC version). Consider...
This is a reasonable (yet not maximal) shrinking of a real-life Agda project: ```agda interleaved mutual data Scope : Set variable sc : Scope data Decls (sc : Scope) :...