Struct TypeChecker 

pub struct TypeChecker { /* private fields */ }

Type checker (trusted kernel)

Implementations

impl TypeChecker

pub fn new() -> Self

Create a new type checker

pub fn infer( &mut self, arena: &mut Arena, levels: &mut LevelArena, env: &Environment, ctx: &Context, term: TermId, ) -> Result<TermId>

Infer the type of a term

This is the heart of the type checker: Γ ⊢ t : ?

pub fn check( &mut self, arena: &mut Arena, levels: &mut LevelArena, env: &Environment, ctx: &Context, term: TermId, expected_ty: TermId, ) -> Result<()>

Check that a term has an expected type

Γ ⊢ t : T (checking mode)

pub fn check_declaration( &mut self, arena: &mut Arena, levels: &mut LevelArena, env: &Environment, decl: &Declaration, ) -> Result<()>

Verify a declaration is well-typed before adding to environment

pub fn converter(&mut self) -> &mut Converter

Get the converter (for advanced use)

Trait Implementations

impl Default for TypeChecker

fn default() -> Self

Returns the “default value” for a type.