Skip to content

Commit

Permalink
[ #7 ] Found the problem: it's trying to check the signature of `leve…
Browse files Browse the repository at this point in the history
…l0`, and because it fallbacks to `check(..., Type(0))` which causes problem.

I need to implement a more formal universe checker
  • Loading branch information
ice1000 committed Mar 16, 2019
1 parent 084a4b8 commit 0439c52
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 1 deletion.
2 changes: 2 additions & 0 deletions samples/basics/univese.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
Parse successful.
Type-Check successful.
1 change: 0 additions & 1 deletion src/check/decl.rs
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,6 @@ pub fn check_simple_declaration(
check_type(index, tcs_borrow!(tcs), signature.clone())
.map_err(|err| try_locate!(err, pattern))?;
let signature = signature.eval(tcs.context());
println!("Signature of {} is: {}", pattern, signature);
check(index, tcs_borrow!(tcs), body.clone(), signature.clone())
.map_err(|err| try_locate!(err, pattern))?;
let TCS { gamma, context } = tcs;
Expand Down

0 comments on commit 0439c52

Please sign in to comment.