Andre Knispel
Andre Knispel
When hlint finds an import that has an unnecessary hiding statement, apply-refact removes the entire statement instead of just removing the unnecessary hidings. For example, in the following code apply-refact...
I have several functions from other files that I use regularly, and even though I can fetch their definitions with M-F12 for example, when I type part of the name...
Consider the following code: ``` agda {-# OPTIONS -v test:10 #-} module ArgTurningIntoUnknown where open import Data.List open import Data.Unit open import Level open import Reflection variable l : Level...
The asterisk ranges over Reconstructed, Normalisation, ExpandLast and ReduceDefs. `withReconstructed` and `withNormalisation` replace their old counterparts, and `onlyReduceDefs` and `dontReduceDefs` have been removed.
Several reflection primitives in Agda simply reflect aspects of the `TCM` monad into Agda, particularly some of its state and environment. There is not much structure to those primitives though,...
This adds some generic code for dealing with (extensional) quotients
PDF-tools doesn't seem to support follow-mode, trying to use it results in the other window displaying the buffer being empty. I don't know what would need to happen for it...
In `examples/containers/module-edits/Data/IntSet/Internal/edits`, there is the following line right at the top: `rename type GHC.Types.Int = Coq.Numbers.BinNums.N` Shouldn't that be `rename type GHC.Types.Int = Coq.Numbers.BinNums.Z`instead?
In a file that I'm generating with hs-to-coq, there appears the line `Require Deriving.`. I don't know why this line is generated (I suspect it is related to the `DeriveGeneric`...
There were some discussions about documentation at AIM XXXVII, and @andreasabel suggested that Agda's documentation could be structured as recommended [here](https://documentation.divio.com), specifically into: - Tutorials - How-to guides - Explanations...