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

level #21

Closed oraluben closed 5 years ago

oraluben commented 5 years ago

Change overview:

  1. The level of Sigma/Pi/Sum will be inferred, there's no change at parser.
  2. Inferring level and update Gamma/telescope in check_declaration.

Something needed helps from reviewer:

  1. I'm not very clear about levels among recursion, please have a look.
  2. I have problem inferring some levels, e.g. code below. I guess the level of Type0 * Type1 should be at the same level of 1, Type0, which is 1. Anyway to determine if a Type is a type or term? 
    :infer Type0 * Type1
Type2
ice1000 commented 5 years ago

I've found a bug in the previous commit, force-pushed a working solution.