When utilizing the old musical coinduction notation, Auto will attempt to fill flat-involved goals with the incorrect projection x .♭, instead of the correct ♭ x.
To replicate: C-c C-a in the hole.
{-# OPTIONS --guardedness #-}
open import Codata.Musical.Notation
data ⊤ : Set where
tt : ⊤
test : ∞ ⊤ → ⊤
test x = {!!}
Produces:
test x = x .♭
Expected:
test x = ♭ 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