Nils Anders Danielsson
Nils Anders Danielsson
I have some code of (roughly) the following form: ```agda mutual f : D → E ⋮ f (c x y) = … lemma₂ y … f x … f...
@andreasabel, consider the following code: ```agda Type : Set postulate type : Type Term : Type → Set Type = Term type ``` When I run Agda with `-vterm.found.call:20` I...
At least it's an explanation. I don't know if it's a problem, you are the expert on termination.
The changelog for 2.6.0 mentions that this bug has been fixed, so I guess it makes sense to document that it has been reintroduced.
> I stumbled upon this problem when trying to understand the metavariable solver, where I found out the occurs check doesn't check for occurrences in the type of a solution:...
With `--profile=internal`: * With 2.6.3: ``` Total 902,327ms Miscellaneous 1,450ms Typing 47,566ms (595,814ms) Typing.CheckRHS 292,151ms Typing.CheckLHS 62,214ms (95,712ms) Typing.CheckLHS.UnifyIndices 33,497ms Typing.OccursCheck 92,441ms Typing.With 29,487ms Typing.Generalize 25,018ms Typing.InstanceSearch 8,556ms Typing.TypeSig 4,879ms...
> Maybe you can disclose your development so that others can try to reproduce your observation. It is [`graded-type-theory`](https://github.com/graded-type-theory/graded-type-theory/tree/8858200068f2c42708bfa9f9879a199fbed99ff0), along with version 1.7.2 of the standard library.
I think `data` should come first, and `higher`/`cubical` after, because `data` is the main concept. I also think that, if possible, we should use the same style as for `record`...
> Then indexed data types without transport would have to be rejected. Another option is perhaps to insert this automatically for indexed types with path constructors.
Coq uses something like this kind of notation, right? Would it be required that the names in the list of parameters are distinct? Is the idea that one should be...