search

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

Merge two sums #15

Closed ice1000 closed 5 years ago

ice1000 commented 5 years ago

Syntax:

let bool: Type = Sum { True } ++ Sum { False };

Things to consider:

ice1000 commented 5 years ago

Currently, I will make this code

rec nat: Type = Sum { Zero | Suc nat };
let unit: Type = Sum { TT };
nat ++ unit

return Sum { TT | Zero | Suc nat }, instead of rec bla: Type = Sum { TT | Zero | Suc bla }; bla.