MWE:
{-# OPTIONS --with-K #-} -- will occur with or without this, also occurs with --without-K
module MWE where
open import Agda.Builtin.Equality using (_≡_)
open import Data.Nat using (ℕ; _≟_)
open import Relation.Nullary using (yes; no)
F : ℕ → ℕ
F p with p ≟ p
... | yes _ = {! !}
... | no _ = {! !}
swap-inj : ∀ {p} → F p ≡ F p → ℕ
swap-inj eq = {! !}
When the cursor is in the last hole and C-c C-a is pressed, agda complains "Not implemented: The Agda synthesizer (Agsy) does not support HITs yet". If --without-K is enabled, then the same code works with Bool.
Agda version 2.6.3, using VSCode on OS X.
jgrosso, laMudri and mietek
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