The following sequence of commands succeeds if Agda 2.7.0.1 is used, but fails with Agda-2.8.0-50c9f1f:
mkdir fresh && cd fresh
(git clone https://github.com/agda/agda-stdlib.git && cd agda-stdlib && git checkout b0505d661fbbfecf7ffeae20cc4b48c8ef41e078)
(git clone https://github.com/nad/equality && cd equality && git checkout f2a3158af4b11912f5cd257ed4a34f205ea644f7)
cat > libraries <<EOF
$PWD/agda-stdlib/standard-library.agda-lib
$PWD/equality/equality.agda-lib
EOF
cat > Bug.agda <<EOF
{-# OPTIONS --erasure #-}
open import Equality.Propositional
open import Prelude
open import Tactic.By.Propositional
open import Maybe equality-with-J
open import Monad equality-with-J
data D : Type where
c : D → D
f : D → Maybe D
f (c x) = just c ⊛ f x
f-just : ∀ x → f x ≡ just x
f-just (c x) =
just c ⊛ ⟨ f x ⟩ ≡⟨ ⟨by⟩ (f-just x) ⟩
just c ⊛ just x ≡⟨⟩
just (c x) ∎
EOF
agda --no-default-libraries --library-file=libraries -lstandard-library -lequality -i. Bug.agda
Bisection points to two commits (because one failed to build): 76b84ff ("Overwrite instance table entry when adding an alias") and 7115e00 ("Block instances on discrimination tree overlap"). @plt-amy, is this change intended?
If f-just is replaced by the following code, then the code is for some reason accepted:
postulate f-just′ : ∀ x → f x ≡ just x f-just : ∀ x → f x ≡ just x f-just (c x) = just c ⊛ ⟨ f x ⟩ ≡⟨ ⟨by⟩ (f-just′ x) ⟩ just c ⊛ just x ≡⟨⟩ just (c x) ∎
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