owo-lang / minitt-rs

Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust
Apache License 2.0
113 stars 3 forks source link

Support "otherwise" in split #2

Open ice1000 opened 5 years ago

ice1000 commented 5 years ago

Expected syntax:

let threee: U = sum { One | Two | Three };
let three: U = sum { Two | Three };

let three_f (a: U) (m: three): 1 = split { Two => 0 | Three => 0 };
let threee_f (a: U) (m: threee): 1 = split { One => 0 | e => (three_f a) e };