Nils Anders Danielsson
Nils Anders Danielsson
Note that, as I wrote above, `cabal-plan` does not list all relevant dependencies.
Perhaps it is possible to "smuggle in" a dependency using `Setup.hs`.
It might also make sense to set [`electric-indent-inhibit`](https://www.gnu.org/software/emacs/manual/html_node/elisp/Auto_002dIndentation.html) to `t`. It seems as if setting `indent-line-function` does not have an effect on what happens when you use "shift tab", so...
Documentation is missing. Is the idea that it should be possible to import modules that use `--cubical-without-glue` from modules that use `--erased-cubical` or `--cubical`?
> This is in anticipation of my ongoing project to implement Cubical with UIP as mentioned in #3750 . Please discuss the design of such a feature before you implement...
I think the documentation should include something about how the options interact (which is [somewhat complicated](https://agda.readthedocs.io/en/v2.7.0.1/language/cubical.html#cubical-agda-with-erased-glue) in the case of `--erased-cubical` and `--cubical`).
That would break quite a bit of code. I don't think we should perform such a change just before the release.
> Each (file) module could have a (file) submodule `.Example` explaining the use of the primitives. The idea was to use the modules under `README` for things like that. Only...
Related: #3198, #4988.
Some comments and questions: * I think it makes sense to have something like this. * You did not give any use cases for definitions. * > Definitions are checked...