open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.List using (List; [])
open import Data.List.Membership.Propositional using (mapWith∈)
postulate X : Set
f : List X → List (List X)
f xs = mapWith∈ xs λ _ → xs
notImplemented : ∀ {ns} → f ns ≡ f ns
notImplemented = {!!} -- ←—— press C-c C-a here
Not implemented: The Agda synthesizer (Agsy) does not support HITs
yet
I didn't manage to get away with the dependency on stdlib, as a manual reimplementation of mapWith∈ in the same module does not cause any problems:
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.List using (List; []; _∷_)
data Any {A : Set} (P : A → Set) : List A → Set where
here : ∀ {x xs} → P x → Any P (x ∷ xs)
there : ∀ {x xs} → Any P xs → Any P (x ∷ xs)
record Setoid : Set₁ where
field
A : Set
_≈_ : A → A → Set
≈-refl : ∀ {a : A} → a ≈ a
module Mem (S : Setoid) where
open Setoid S
_∈_ : A → List A → Set
x ∈ xs = Any (_≈ x) xs
mapWith∈ : ∀ {B : Set} (xs : List A) → (∀ {x} → x ∈ xs → B) → List B
mapWith∈ [] f = []
mapWith∈ (x ∷ xs) f = f (here ≈-refl) ∷ mapWith∈ xs (λ p → f (there p))
postulate X : Set
open Mem (record {A = X; _≈_ = _≡_; ≈-refl = refl})
f : List X → List (List X)
f xs = mapWith∈ xs λ _ → xs
notImplemented : ∀ {ns} → f ns ≡ f ns
notImplemented = {!!} -- ←—— press C-c C-a here, returns `refl` as expected
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