Andreas Abel

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 for...

@mergifyio rebase

@nad, it would be probably easy to print the second error as: ``` Could mean any one of: ⟨_⟩ (? □) ⟨_⟩ (_□ ?) ``` Just switch off operator reconstruction....

> What is "operator reconstruction"? This is a phase in `AbstractToConcrete` responsible for printing `1 + 2` instead of just `_+_ 1 2`. But anyway, this is not relevant here...

For instance, we could add the error id to the pragma ``` {-# ERROR NoSuchModule open BogusModule #-} ```

Current error (after #5730 has been improved) is more benign: ``` Cannot generate inferred clause for congω. Case to handle: congω f (Agda.Primitive.Cubical.primHComp {.Agda.Primitive.lzero} {.(_ ≡ _)} {φ = φ}...

Some related issues: - #154 - #2862

Here is a slight variation without holes: ```agda {-# OPTIONS --without-K #-} open import Agda.Primitive open import Agda.Builtin.Sigma open import Agda.Builtin.Unit open import Agda.Builtin.Equality postulate ANYω : ∀ {A :...

Github isn't good at understanding negations... ;-) I wrote > Unfortunately, this refinement does not fix https://github.com/agda/agda/issues/6008. and it matched `fix #6008` and closed this issue. Maybe I should have...

```agda ---------------------------------------------------------------------- -- Copyright: 2013, Jan Stolarek, Lodz University of Technology -- -- -- -- License: See LICENSE file in root of the repo -- -- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps --...