RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/7811 below:

Internal error with Path and with-abstraction II · Issue #7811 · agda/agda · GitHub

When debugging #7803 I found another issue:

open import Agda.Builtin.Cubical.Path

p : Set ≡ Set
p i with Set _
... | _ = Set

This bug has been sleeping since the code was original written, the error not (freeIn 0 s) rather than not (freeIn 0 l) exists already in the first version of the code.

getLevel b = do s <- reduce $ getSort <$> b case s of NoAbs _ (Type l) -> return l Abs n (Type l) | not (freeIn 0 s) -> return $ noabsApp __IMPOSSIBLE__ (Abs n l)

I can reproduce this internal error e.g. with Agda-2.6.2.

Ref:

Internal error with Path and with-abstraction #7803

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4