The Inductive instance for

The following doesn't work either: <div class="highlight highlight-source-agda not

<div class="snippet-clipboard-content notranslate position-relative overflow-auto" data-snippet-clip

Fixed by <a class="issue-link js-issue-link" data-error-text="Failed to load title" da

Can't eliminate truncation inside `absurd` about 1lab HOT 3 CLOSED

ncfavier commented on August 23, 2024

Can't eliminate truncation inside `absurd`

from 1lab.

Comments (3)

ncfavier commented on August 23, 2024

The following doesn't work either:

bad : ∥ ⊤ ∥ → ⊥
bad t = absurd (∥-∥-rec (hlevel 1) {!   !} t)
{-
H-Level: There are no hints for treating the name ⊥ as a projection.
When showing that the type
 ⊥
has h-level 1.
-}

It seems like irrelevance is really messing with instance search, so this should probably go on the Agda tracker...

from 1lab.

ncfavier commented on August 23, 2024

{ dropSameCandidates
instances after resolving overlap:
- INCOHERENT H-Level-projection : {ℓ : Level} {A : Type ℓ}
                                  {n : Nat} {@(tactic hlevel-proj A n) inst : is-hlevel A n} →
                                  H-Level A n
- H-Level-⊥ : {n : Nat} → H-Level ⊥ (suc n)
dropSameCandidates: Meta is irrelevant so any candidate will do.
}
  valid candidates
  - INCOHERENT H-Level-projection : {ℓ : Level} {A : Type ℓ}
                                    {n : Nat} {@(tactic hlevel-proj A n) inst : is-hlevel A n} →
                                    H-Level A n
}

👀

from 1lab.

ncfavier commented on August 23, 2024

Fixed by agda/agda#7364

from 1lab.

Recommend Projects