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

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

Uncaught pattern violation when using `with...in...` instead of old-school inspect · Issue #6841 · agda/agda · GitHub

The following code typechecks with inspect, but panics when using with...in...:

open import Data.Maybe
open import Relation.Binary.PropositionalEquality

postulate A : Set; x : A

withIn-bug : A
withIn-bug
--   with just x | inspect just x
-- ... | just y | [ eq ]
  with just x in eq
... | just y
  = y

Panic: uncaught pattern violation

(Andreas:)
Related:

• "Panic: uncaught pattern violation" involving holes and with #5805

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