search

fmease / lushui

The reference compiler of the Lushui programming language
Apache License 2.0
5 stars 0 forks source link

Syntax to mark impossible (case analysis) cases #89

Open fmease opened 3 years ago

fmease commented 3 years ago

Meta: Expand.

Example

it: Result Nat Void = success 90
check: Nat = case it of
    success \val => val
    failure \_fail impossible ;;; could've been left off

Undecided: Name of the keyword or syntax in general.

Alt syntax:

it: Result Nat Void = success 90
check: Nat = case it of
    success \val => val
    @impossible (failure \_fail) ;;; no body + attribute analogously to foreign decls etc.
fmease commented 3 years ago

Agda-style (takes away ()):

check (it: Result Nat Void): Nat =
    case it of
        success \it => it
        failure \_ ()