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

Infer type of constructor call as a "minimum sum" #3

Closed ice1000 closed 5 years ago

ice1000 commented 5 years ago

Currently:

=> :load samples\sum-split\maybe.minitt
=> :gamma
Current Gamma:
maybe: Π _: U. U
the: Π t: U. Π _: t. t
unwrap: Π t: U. Π mt: (maybe t). ((unwrap_type t) mt)
unwrap_type: Π t: U. Π _: (maybe t). U
=> :type unwrap (Just 1)
Cannot infer type of: `Just 1`.
At unknown location.
=> :type unwrap (Just 0)
Cannot infer type of: `Just 0`.
At unknown location.