Nils Anders Danielsson

Another option would be to use `MonadFail`.

The [hasktags program](https://hackage.haskell.org/package/hasktags) does not depend on [ghc](https://hackage.haskell.org/package/ghc). This, along with the [list of hasktags issues](https://github.com/MarcWeber/hasktags/issues), suggests to me that the program does not use a proper Haskell parser.

Now there are some alternatives: * "[ghc-tags: Utility for generating ctags and etags with GHC API.](https://hackage.haskell.org/package/ghc-tags)" * "[ghc-tags-plugin: A compiler plugin which generates tags file from GHC parsed syntax tree.](https://hackage.haskell.org/package/ghc-tags-plugin)"

I used `{doc}id` instead of `id;comment`. If feature request #5541 is implemented, then we could use these identifiers for the proper documentation comments instead: the heuristic that I implemented does...

> Perhaps it would also be nice to (optionally) make all generated links target comments rather than code (but see #2756). I moved this part to issue #5974.

During the Agda meeting today we discussed disallowing the combination of `--cubical` and `--prop`, because little thought seems to have gone into the combination of these features (see issue #5816)....

Some thoughts: * A disadvantage of this kind of feature is that it might make it harder to read Agda code. However, the idea seems to be to make it...

> I observe that when `Set` is renamed to `Type`, the old meaning of `Set` doesn't go away, and in particular it is not available to be given other meanings....

> In analogy to pattern lambda, a natural symbol to replace `=` would be the right arrow `->`. I don't want to read or write `Relation A → A →...

> Thanks for chiming in, @Saizan. Current `master` contributes indexed inductive types to Cubical Agda, but the development isn't finished yet. We need a plan what to do about it...