Expand description
A type checker for the kind2 language. It has some utilities to compile kind2 code into a version that the checker can understand and transform the answer back into a version that the Rust side can manipulate.
Modules§
- compiler
- This module compiles all of the code to a format that can run on the HVM and inside the checker.hvm file.
- report
- Transforms a answer from the type checker in a Expr of the kind-tree package.
Constants§
Functions§
- eval
- eval_
api - Runs the type checker but instead of running the check all function we run the “eval_main” that runs the generated version that both HVM and and the checker can understand.
- gen_
checker - Generates the checker in a string format that can be parsed by HVM.
- type_
check - Type checks a dessugared book. It spawns an HVM instance in order to run a compiled version of the book