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

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

Internal error when calling MakeCase on target `__` · Issue #7863 · agda/agda · GitHub

I tried to invoke MakeCase on __ to see if it does anything, and it caused an internal error inside Agda.

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full\Agda\Syntax\Concrete\Name.hs:276:23 in Agda-2.7.0.1-8637b2a2180054048437c826d64d19d3f344c63d:Agda.Syntax.Concrete.Name

1. Create a file Reporducer.agda with the following content:

module Reproducer where
    data Bool : Set where 
        false : Bool
        true : Bool

    _^_ : Bool -> Bool -> Bool
    _^_ = {! __ !}

1. In the IDE, place your cursor in the hole at line 7 and invoke MakeCase by pressing C-c C-c
2. Agda prints the error message

1. Create a file Reporducer.agda with the following content:

module Reproducer where
    data Bool : Set where 
        false : Bool
        true : Bool

    _^_ : Bool -> Bool -> Bool
    _^_ = {!  !}

1. In the IDE, place your cursor in the hole at line 7 and invoke MakeCase by pressing C-c C-c
2. You are prompted for a variable to split, type __ and press enter
3. Agda prints the error message

• Agda 2.7.0.1
• GHC 9.6.7
• Windows 10 Family Edition, build 19045.5737
• VSCode 1.99.3 with agda-mode 0.5.6

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