Skip to content

Tactics' agda-split can destroy matches #1426

Closed
@isovector

Description

@isovector

data ADT = One | Two Int | Three | Four Bool ADT | Five

case_split :: ADT -> Int
case_split One = _
case_split (Two i) = _
case_split Three = _
case_split (Four b a) = _  -- here
case_split Five = _

Splitting on either b or a at -- here deletes the entire case_split (Four b a) match.

Metadata

Metadata

Assignees

No one assigned

    Labels

    component: wingmantype: bugSomething isn't right: doesn't work as intended, documentation is missing/outdated, etc..

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions