Skip to content
Snippets Groups Projects
Select Git revision
  • 99-add-let-binder
  • main default protected
  • 108-opaque-traces
  • 115-improve-ci-by-using-nix
  • 106-logsem-seminar-talk
  • 109-feat-tilleul-add-vscode-support
  • 111-non-dependent-products-optimisation
  • 81-bug-parser-no-error-when-defining-a-declaration-with-the-same-name-as-a-definition
  • 110-unhandled-lsp-requests-declared-as-capabilities-in-tilleul
  • 107-parser-simplification
  • 95-replace-succ-with-an-add-constructor-on-level
  • 102-add-match-syntax
  • 105-specialize-traces
  • 66-implement-bidirectional-type-checking
  • 104-implement-normalisation-by-evaluation
  • 98-parsing-building-allow-left-arguments
  • 91-add-examples-as-a-test-suite-for-the-pipeline
  • 52-add-better-tab-behavior-for-proost-toplevel
  • 103-normal-form-memoization
  • 97-preparations-for-v0-3-0
  • v0.3.0
  • v0.2.0
  • 0.1.0
23 results
Compare History
belazy's avatar
9-add-a-basic-type-checker ✨️
belazy authored 
Closes #9 🐔️👍️

🦀️🍰🦀️🍰🦀️🍰

* Fix : clippy

* Chore : document `TypeCheckingError`

* Chore : remove useless mut

* Feat : make `Context` private

* Feat : simplify `check`

* Chore : Remove old comment

* Chore : remove eta-expansion for functions to please the big guy

* Chore : comment error

* Chore : remove `println`

* Chore : add doc for `TypeCheckingError`

* Fix : put derive before comments

* Feat : add more coverage

* Fix : golf `whnf()`

* Fix : `polymorphism` test

* Fix : `pub_crate` for  `substitute`

* Chore : CamelCase

* Feat : add `Type_checking_error`

* Chore : move `normal_form` and `whnf` to `term.rs`

* Chore : rename tests

* Chore : remove debug `println`

* Chore : Add documentation

* Feat : use `whnf()` instead of `normal_form()` for conversion

* Chore : resolve ill-typed `complex_subst` test

* Feat : remove `Val`, correctly substitute terms.

* Chore : remove `classic_term.rs`

* chore(Context): Rename

* chore(type_checker): Apply clippy suggestions on tests

* fix: Remove Term's Abs/Prop names

* chore: format + derive Default for Ctx

* chore: Reorganise type_checker + derive Default for Ctx

* Feat : add documentation for `type_checker.rs`

* Chore: merge `impl Val`s

* Chore : remove debug prints in tests

* Chore : mark `Err`s with `//TODO #19`

* Chore : Move `Val` to the top of the file

* Fix :  remove `set_var` in tests

* Fix : `polymorphism` test

* chore: move everything to their respective `impl`

* fix: avoid `assert` in `is_def_eq`, move Val-related methods

* chore : make `conversion` a method

* Fix: make `normal_form` a method

* fix:  use `self` for `eval`

* Fix : Add issue reference

* Feat : remove `panic!`s, use `Result` monad instead

* Chore : rename `Ctx::empty()` to `Ctx::new()`

* Chore : remove duplicate `assert_def_eq`

* Chore : add `impl Term`

* Chore : remove `use Term::*`, add `use Val::*` instead

* Chore : remove `Into` trait for UniverseLevel

* remove useless `impl` for `UniverseLevel`

* Chore : remove prints

* fix : comment `Val`

* Fix : make `conv` into an `Into` trait

* fix : `Val` constructor names

* fix : imports

* chore : fix TODO

* fix : `lib.rs` imports

* fix : inference for lambda-abstractions

* chore : remove useless print

* chore : fix various comments

* fix : `is_universe`

* chore : add more comments to `conv`

* feat : simplify `quote`

* chore : add TODO

* fix : commentary for beta_reduction

* chore : comment Val

* chore : remove old comment

* fix : added `Ctx` type to store type of Vars during checking

* feat :  add polymorphic test which shows the need to add `Ctx`

* chore : please Clippy

* Fix : stop cloning environments for no reason

* fix : test

* chore : add comments

* feat : add `check` and `infer`

* fix: add string data to lambda-pi abstractions from classicTerm

* feat: add string data to pi/lambda-abstractions

* fix : made clippy happier

* chore : adapt existing code to rebase

* fix : conversion between Var and VVar

* fix : remove complex_subst from the def_eq test suite for now

* feat : added Ctx in preparation for type-checking

* this pleases the formatter

* Fix : conversion algorithm

* basic conversion algorithm (doesn't work)
1b895235
Name Last commit Last update
docs
kernel
parser
proost
.gitattributes
.gitignore
.gitlab-ci.yml
Cargo.lock
Cargo.toml
LICENSE.md
README.md
flake.lock
flake.nix
README.md

Proost

A simple proof assistant written in Rust.

Development environment

With nix installed, simply type nix develop. This provides an environment with all the necessary tools, including clippy and rustfmt. There, it is possible to run the usual cargo build and so on.

Please consider the syntax nix develop --profile <a-file-of-your-choosing>, which will prevent the garbage collection of the development dependencies.

Build and install

With nix installed, type nix build to perform a build and have it in the nix store. One can also type nix profile install in the repo to install proost to your profile and use it everywhere!