Skip to content

Tactics: case split as several declarations #582

Closed
@serras

Description

@serras

Right now, if I start with the following code:

go :: Maybe Int -> Int
go x = _

and use "case split on x", the result is:

go x = (case x of
   Nothing -> _
   (Just i) -> _)

which is not very idiomatic. I was wondering whether there's room for a new "case split" which would produce:

go Nothing = _
go (Just i) = _

@isovector do you have any opinions on this? I am happy to invest some time on implementing this, but I don't want to step over anybody's plans.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions