Nils Anders Danielsson
Nils Anders Danielsson
Agda generates incorrect HTML for the following code: ```agda module _ where module A where postulate A : Set ``` The [W3C Markup Validation Service](https://validator.w3.org/) complains about "Duplicate ID A"....
The new implementation of the HTML backend uses numbered links for definitions in anonymous modules. In many (all?) cases it should be fine to use named links for these definitions...
Currently we have the following 'NameKind's: https://github.com/agda/agda/blob/1b44372081e5b21b1a368d0e63cc09a53c48d20b/src/full/Agda/Interaction/Highlighting/Precise.hs#L94-L109 Now consider the following code: ```agda module _ where module M where _ : let module N = M; A = Set in...
The flag `--two-level` is not mentioned in the documentation.
It would be nice with proper support for inductive families in Cubical Agda. If I have understood correctly this is a non-trivial research problem, so I have put this issue...
Consider the following code: ```agda open import Agda.Builtin.Bool F : Bool → Set F true = Bool F _ = Bool ``` This code is accepted by Agda, but rejected...
Let's say that we have the following code: ```agda postulate □ : Set _□ : Set → Set ⟨_⟩ : Set → Set ``` In this setting the following ambiguous...
@jamesmckinna noticed a lack of lemmas relating renamings and substitutions, and I added some.
Consider the type of the [`hfill`](https://github.com/agda/cubical/blob/8391a4835b3d2478e9394c6c3ec7e6fff42ede62/Cubical/Core/Primitives.agda#L160-L170) operation from the cubical library: ```agda {A : Type ℓ} {φ : I} (u : ∀ i → Partial φ A) (u0 : A...