crude but effective stratification #7

New Issue

Closed

opened 2023-04-19 15:32:50 -04:00 by rhi · 3 comments

rhi commented

2023-04-19 15:32:50 -04:00

Owner

No description provided.

rhi commented

2023-05-21 14:37:51 -04:00

Author

Owner

✅

rhi closed this issue

2023-05-21 14:37:51 -04:00

rhi commented

2023-07-21 12:02:05 -04:00

Author

Owner

--          works if this is List¹
--                                 ↘
def0 All : (A : ★) → (P : A → ★) → List A → ★ =
  λ A P ⇒ foldr¹ A ★ True (λ x ps ⇒ P x × ps);

while checking that
  caseω len
  return ★¹  -- ←
  of { zero ⇒ {nil}; succ _, 0.Tail ⇒ (((A ∷ ★¹) ∷ ★¹) ∷ ★¹) × Tail }
is a supertype of
  caseω len
  return ★⁰ -- ←
  of { zero ⇒ {nil}; succ _, 0.Tail ⇒ ((A ∷ ★⁰) ∷ ★⁰) × Tail }
in context 0.A : ★⁰, 0.P : 1.A → ★⁰, 0.len : ℕ

the universe level 1 is not equal to 0

``` -- works if this is List¹ -- ↘ def0 All : (A : ★) → (P : A → ★) → List A → ★ = λ A P ⇒ foldr¹ A ★ True (λ x ps ⇒ P x × ps); ``` ``` while checking that caseω len return ★¹ -- ← of { zero ⇒ {nil}; succ _, 0.Tail ⇒ (((A ∷ ★¹) ∷ ★¹) ∷ ★¹) × Tail } is a supertype of caseω len return ★⁰ -- ← of { zero ⇒ {nil}; succ _, 0.Tail ⇒ ((A ∷ ★⁰) ∷ ★⁰) × Tail } in context 0.A : ★⁰, 0.P : 1.A → ★⁰, 0.len : ℕ the universe level 1 is not equal to 0 ```

rhi reopened this issue

2023-07-21 12:02:07 -04:00

rhi added the

bug

language

labels 2023-07-21 12:02:17 -04:00

rhi changed title from ~~crude but effective stratification (probably)~~ to crude but effective stratification

2023-07-21 12:02:35 -04:00

rhi commented

2023-07-22 15:28:01 -04:00

Author

Owner